I don't understand why you are invested in nitpicking the work of an anonymous 7th grader from decades ago. Clearly, filling in all of the details of any forma

I don't understand why you are invested in nitpicking the work of an anonymous 7th grader from decades ago. Clearly, filling in all of the details of any formal proof in Greek style is going to require a careful knowledge of the axioms in use and some list of previously proven theorems which are allowed to be used without re-proof. Depending on which theorems are at hand already, one or another proof might be shorter or longer or more or less obvious. When trying to construct a whole mathematical treatise, the best order for the theorems so that each proof depends only on previously proven theorems is a tricky choice involving some trade-offs between pedagogical goals and concision of individual proofs. But all of that is missing the point.