Gérard's suggestions regarding triangles in the complex plane

[nmegill]

Gérard sent me the following suggestions regarding this. It sounds ok to me but I'm posting it in case there are any comments.

" Following Mario’s proof of Heron’s formula, I propose the following change in set.mm : 1: The current section « 14.3.5 : Theorems of Pythagoras, isoceles triangles and intersecting chords » would become « 14.3.5 Triangles in the complex plane: theorems of Pythagoras and isoceles and Heron’s formula »; 2: Simultaneously, a new section « 14.3.6 Intersecting chords theorem" would be created containing the six current theorems chordthmlem (21693) to chordthm (21698) that are forming David Moews’s proof of this theorem. "

[tirix]

I have no objections.

[benjub]

Or maybe: 14.3.5. Elementary plane geometry 14.3.5.1. Angles 14.3.5.2. Law of cosines and theorem of Pythagoras 14.3.5.3. Theorem of the isosceles triangle 14.3.5.4. Intersecting chords theorem 14.3.5.5. Heron's formula

Remarks:

• I think it's important that the word "angle" appear in the TOC and have its own subsection. Similarly, "law of cosines" should appear in the TOC, and it naturally goes with Pythagoras (which is proved as a special case of it).
• If one prefers, one may name the section "Elementary plane geometry: triangles and chords".
• In isosctrlem3 and isosctr, there is one extra hypothesis for the nondegeneracy of the triangle: in the lemma, if A \neq 0 and |A|=|B|, then assuming B \neq 0 is superfluous; similarly in the theorem.
• Actually, a better option would be to leave these hypotheses and prove the equivalence of equality of side lengths with equality of angles...