proposition: Lemma isosceles_conga : A<>C -> A<>B -> isosceles A B C -> CongA C A B A C B.
proof: Proof. intros. apply cong3_conga. auto. auto. unfold Cong_3. unfold isosceles in H. repeat split;Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect