proposition: Lemma equilateral_strict_equilateral : equilateral_strict A B C -> equilateral A B C.
proof: Proof. unfold equilateral_strict in *. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect