proposition: Lemma equilateral_strict__not_col : equilateral_strict A B C -> ~ Col A B C.
proof: Proof. intros. assert (T:=(equilateral_strict_neq H)). unfold equilateral_strict in *. unfold equilateral in *. spliter. intro. assert (Midpoint B A C) by (apply (l7_20_bis B A C);finish). assert (Midpoint C A B) by (apply (l7_20_bis C A B);finish). apply midpoint_not_midpoint with C A B;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect