proposition: Lemma equilateral_strict_swap_5 : equilateral_strict A B C -> equilateral_strict C B A.
proof: Proof. intros. assert (T:= equilateral_strict_neq H). unfold equilateral_strict in *. intuition (eauto with equilateral). Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect