proposition: Lemma bet_1D' (a b c : 'rV[R]_1) : a 0 0 - c 0 0 != 0 -> 0 < (b 0 0 - a 0 0) / (c 0 0 - a 0 0) < 1 -> bet a b c.
proof: Proof. move=> NE /andP[HGt HLt]; rewrite /bet /betS. have: (betR (a 0 0)%:M (b 0 0)%:M (c 0 0)%:M = (b 0 0-a 0 0) / (c 0 0-a 0 0)). apply ratio_eq; rewrite -[(a 0 0) %:M]scalemx1 -1?[(b 0 0)%:M]scalemx1; rewrite -[(c 0 0)%:M]scalemx1 -!scalerBl ?scalerA ?scalemx_eq0 ?negb_or; rewrite ?matrix_nonzero1 ?andbT -1?mulrAC -?mulrA ?divff ?mulr1 //; by rewrite subr_eq0 eq_sym -subr_eq0. rewrite -!mx11_scalar. move=> ->. rewrite HLt HGt !andbT. apply /orP; right. apply /eqP/matrixP=> i j. by rewrite !ord1 !mxE /= mulrAC -mulrA divff ?mulr1 // subr_eq0 eq_sym -subr_eq0. 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