proposition: Lemma segment_construction : ~ segment_constructionP Point Bet Cong.
proof: Proof. unfold segment_constructionP, Bet; intro H. destruct (H P0 P0 P0 P0) as [E [HBet _]]; tauto. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence