proposition: Lemma five_segment : five_segmentP Point Bet Cong.
proof: Proof. unfold five_segmentP, Bet, Cong. intros A A' B B' C C' D D' HCong1 HCong2 HCong3 HCong4 [H|H] HBet2 HNEq; [contradiction|subst]. destruct HCong1 as [H|[H1 H2]]; [contradiction|subst]. destruct HCong4 as [H|[H1 H2]]; [auto|subst]. destruct HBet2 as [H|H]; [intuition|subst; tauto]. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence