proposition: Lemma betR_abk (a b: 'rV[R]_(2)) (k : R) : 0 < k -> k < 1 -> b!=a -> betR a b ((1/k)*:(b-a)+a) = k.
proof: Proof. move => kgt0 klt1 bneqa. set c := ((1/k) *: (b - a) + a). have: (b = k*:(c-a)+a). rewrite /c -addrA subrr addr0 scalerA mul1r. rewrite divff ?lt0r ?lt0r_neq0 ?kgt0 //. by rewrite scale1r addrAC -addrA subrr addr0. move->. apply betR_akb; rewrite //. rewrite /c -subr_eq0 -addrA subrr addr0 scalemx_eq0. rewrite subr_eq0. move/negPf: bneqa ->. rewrite mul1r invr_eq0. move:kgt0. rewrite lt0r. by move=> /andP[/negPf -> _]. 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 algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence