proposition: Lemma equilateral_isosceles_3 : equilateral A B C -> isosceles C A B.
proof: Proof. intros. apply equilateral_cong in H. unfold isosceles. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect