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