proposition: Lemma segment_construction : segment_constructionP (@Point R) (@bet' R) (@cong' R).
proof: Proof. move=> a b c d. destruct (@segment_construction R _ (a 0 0)%:M (b 0 0)%:M (c 0 0)%:M (d 0 0)%:M) as [x [HxB HxC]]. destruct (@segment_construction R _ (a 0 1)%:M (b 0 1)%:M (c 0 1)%:M (d 0 1)%:M) as [y [HyB HyC]]. exists (row2 (x 0 0) (y 0 0)). rewrite /bet' /cong' !mxE /=. rewrite [x]mx11_scalar in HxB HxC. rewrite [y]mx11_scalar in HyB HyC. by split; apply /andP; split. 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.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence