proposition: Lemma bet_012 : @bet R 1 0%:M 1%:M (1+1)%:M.
proof: Proof. have eq0P : 0%:M = 0 by move => *; apply/matrixP => i j; rewrite !mxE// mul0rn. apply /orP; right; rewrite -scalemx1 -scalemx1 -[(1+1)%:M]scalemx1 ?eq0P. rewrite /betS /betR ?scale0r !subr0 scale1r /ratio. case: pickP=> [x _|HF]; [|move: (HF 0)]; rewrite ?ord1 !mxE eqxx !mulr1; rewrite ?add11_neq0 // mul1r !scalerA 1!mulrC divff ?add11_neq0 ?eqxx //=. rewrite ?scale1r ?eqxx//. by rewrite invf_lt1 -1?{3}[1]add0r ?invr_gt0 ?addr_gt0 ?ltr_add2r ?ltr01. 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