proposition: Lemma segment_construction a b c d : exists e, bet a b e /\ cong b e c d.
proof: Proof. have [->|neq_ba] := eqVneq b a; [|move: neq_ba; rewrite -subr_eq0=> neq_ba]. exists ((c - d) + a); rewrite /bet /cong betE_xxa; split=> //. by rewrite -!addrA subrr addr0 -opprB mulNmx eq_sym dotC opprB -mulNmx opprB. have [->|neq_dc] := eqVneq d c ; [|move: neq_dc; rewrite -subr_eq0=> neq_dc]. by exists b; rewrite /bet /cong betE_axx !subrr mul0mx eqxx; split. exists (normv(d - c) / normv(b - a) *: (b - a) + b); rewrite /bet /cong; split. rewrite /betS /betR; apply/orP; right; rewrite -addrA. rewrite -[X in _ *: _ + X]scale1r -scalerDl scalerA -ratio_bet'' ?mulVf; rewrite ?scale1r ?eqxx ?invr_gt0 ?invf_lt1 ?lt0r_neq0 -1?{2}[1]add0r; rewrite ?ltr_add2r ?addr_gt0 ?ltr01 1?eq_sym -1?subr_eq0 //= divr_gt0 //; by rewrite sqrtr_gt0 lt0r quad_neq0 quad_ge0 ?neq_ba ?neq_dc. rewrite -addrA subrr addr0 -scalemxAl dotC -scalemxAl scalerA mulf_div -!expr2. rewrite [X in _ *: X == _]mx11_scalar !sqr_sqrtr ?quad_ge0 // -!scalerA. by rewrite scale_scalar_mx mulrC divff ?quad_neq0 // scalemx1 -mx11_scalar. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq order) mathcomp(fintype bigop) mathcomp(ssralg ssrnum matrix) mathcomp(zmodp) GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Meta_theory.Counter_models.coplanarity GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel_inter_dec