proposition: Lemma conga3_equilateral : forall A B C, ~ Col A B C -> CongA B A C A B C -> CongA A B C B C A -> equilateral A B C.
proof: Proof. intros. assert (isosceles B C A) by (apply conga_isosceles;CongA;Col). assert (isosceles C A B) by (apply conga_isosceles;CongA;Col). unfold isosceles in *. unfold equilateral. split;eCong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect