proposition: Lemma equilateral_strict_conga_2 : forall A B C, equilateral_strict A B C -> CongA B A C A B C.
proof: Proof. intros. apply equilateral_strict_swap_1 in H. apply equilateral_strict_conga_1 in H. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect