proposition: Lemma bet_1Di a b c i : a 0 i <= b 0 i -> b 0 i <= c 0 i -> bet (a 0 i)%:M (b 0 i)%:M (c 0 i)%:M.
proof: Proof. rewrite !le_eqVlt; case: (a 0 i =P b 0 i)=> [->|_]; rewrite ?bet_xxa //=. case: (b 0 i =P c 0 i)=> [->|_]; rewrite ?bet_axx //= => HLt HGt. have: (0 < c 0 i - a 0 i)=> [|ac_lt]; first by rewrite subr_gt0 (lt_trans HLt). have: (0 < (b 0 i-a 0 i) / (c 0 i-a 0 i)); [|move: HLt=> _ HLt]. by rewrite ltr_pdivl_mulr // mul0r subr_gt0. have: ((b 0 i-a 0 i) / (c 0 i-a 0 i) < 1); [|move: HGt=> _ HGt]. by rewrite ltr_pdivr_mulr // mul1r ltr_subr_addr addrAC -addrA subrr addr0. have: (betR (a 0 i)%:M (b 0 i)%:M (c 0 i)%:M = (b 0 i-a 0 i) / (c 0 i-a 0 i)). by apply ratio_eq; rewrite -[(a 0 i) %:M]scalemx1 -1?[(b 0 i)%:M]scalemx1; rewrite -[(c 0 i)%:M]scalemx1 -!scalerBl ?scalerA ?scalemx_eq0 ?negb_or; rewrite ?matrix_nonzero1 -1?mulrAC -?mulrA ?divff ?lt0r_neq0 // mulr1 eqxx. rewrite /bet /betS=> ->; rewrite HLt HGt -[(a 0 i) %:M]scalemx1; rewrite -[(b 0 i)%:M]scalemx1 -[(c 0 i)%:M]scalemx1 -!scalerBl ?scalerA; by rewrite -mulrAC -mulrA divff ?mulr1 ?eqxx ?orbT // lt0r_neq0. 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