proposition: Lemma equilateral_strict_neq : equilateral_strict A B C -> A <> B /\ B <> C /\ A <> C.
proof: Proof. intros. unfold equilateral_strict, equilateral in H. decompose [and] H;clear H. repeat split;Cong. eauto using cong_diff. eapply cong_diff. assert (T:=cong_transitivity A B B C C A H2 H3). apply H1. assert (T:=cong_transitivity A B B C C A H2 H3). Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect