proposition: Lemma A10_segment_construction : segment_constructionP (@Point R) (@bet' R) (@cong' R).
proof: Proof. move=> a b c d; rewrite /bet'; case (a =P b)=> [->|_]. case: (b 0 1 =P 0)=> [Hb1|_]; [exists (row2 (b 0 0) (normv(d - c)))|]. rewrite bet_xxa /= /cong' congP_aux /sqr_L2_norm_2D !mxE /=; split. case: (normv (d - c) =P 0)=> /= [->|//]; by rewrite vector2_eq !mxE Hb1 !eqxx. rewrite subrr Hb1 subr0 expr0n add0r /normv congP_aux' /sqr_L2_norm_2D. by rewrite mxE eqxx mulr1n sqr_sqrtr // addr_ge0 ?sqr_ge0. by destruct (segment_construction b b c d) as [E HE]; exists E; rewrite andbT. by destruct (segment_construction a b c d) as [E HE]; exists E; rewrite andbT. 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