proposition: Lemma five_segment : five_segmentP Point bet' cong'.
proof: Proof. move => a a' b b' c c' d d' H1 H2 H3 H4 /andP [H5 _] /andP [H6 _] H7. by apply (@five_segment R 2 a a' b b' c c' d d'). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra) mathcomp(zmodp) GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence