proposition: Lemma equilateral_strict_conga_1 : equilateral_strict A B C -> CongA C A B A C B.
proof: Proof. intros. assert (T:= equilateral_strict_neq H). apply equilateral_strict_equilateral in H. apply equilateral_isosceles_1 in H. apply isosceles_conga. tauto. tauto. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect