proposition: Lemma equilateral_cong: equilateral A B C -> Cong A B B C /\ Cong B C C A /\ Cong C A A B.
proof: Proof. unfold equilateral;intros;intuition Cong. assert (T:=cong_transitivity A B B C C A H0 H1). Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect