proposition: Lemma betR_akb (a b: 'rV[R]_(2)) (k : R) : 0 < k -> k < 1 -> b!=a -> betR a (k*:(b-a) + a) b = k.
proof: Proof. move=> kgt0 klt1 bneqa. rewrite /betR /ratio. case: pickP => /= [x|/all_v_neq0 H]. rewrite -addrA subrr addr0. rewrite !mxE /=. move=> ba_neq0. by rewrite -mulrA divff ?mulr1. by exfalso; apply H; rewrite subr_eq0 bneqa. 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