proposition: Lemma bet_1D (a b c : Point) i : a 0 i - c 0 i != 0 -> 0 < (b 0 i - a 0 i) / (c 0 i - a 0 i) < 1 -> bet (a 0 i)%:M (b 0 i)%:M (c 0 i)%:M.
proof: Proof. move=> NE /andP[HGt HLt]; rewrite /bet /betS. 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)). 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 ?andbT -1?mulrAC -?mulrA ?divff ?mulr1 //; by rewrite subr_eq0 eq_sym -subr_eq0. move=> ->; rewrite HLt HGt !andbT -[(a 0 i) %:M]scalemx1 -[(b 0 i)%:M]scalemx1. rewrite -[(c 0 i)%:M]scalemx1 -!scalerBl ?scalerA -mulrAC -mulrA divff ?mulr1; by rewrite ?eqxx ?orbT // 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