proposition: Lemma segment_construction : segment_constructionP Point Bet Cong.
proof: Proof. unfold segment_constructionP, Bet, Cong. destruct A, B, C, D; try (exists P0; solve [intuition discriminate]); try (exists P1; solve [intuition discriminate]); exists P2; intuition discriminate. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence