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