proposition: Lemma col_1D (a b c : 'rV[R]_1) : (bet a b c \/ bet b c a \/ bet c a b).
proof: Proof. suffices: ([ || bet a b c, bet b c a | bet c a b]). by move => /or3P[]; tauto. case: (a =P b) => [-> |/eqP NE1]; rewrite ?bet_xxa //. case: (b =P c) => [-> |/eqP NE2]; rewrite ?bet_xxa ?bet_axx //. case: (c =P a) => [-> |/eqP NE3]; rewrite ?bet_xxa ?orbT //. move: NE1 NE2 NE3. rewrite !mx11_eq. rewrite -subr_eq0 => NE1. rewrite -subr_eq0 => NE2. rewrite -subr_eq0 => NE3. elim (ratio_cp NE1 NE2 NE3). move => H . move: NE3. rewrite subr_eq0 eq_sym -subr_eq0 => NE3. by move: (bet_1D' NE3 H)=> ->. elim. move => H. move: NE1. rewrite subr_eq0 eq_sym -subr_eq0 => NE1. move: (bet_1D' NE1 H)=> -> /=. apply /orP. by right. move => H. move: NE2. rewrite subr_eq0 eq_sym -subr_eq0 => NE2. move: (bet_1D' NE2 H) => ->. apply /orP. right. apply /orP. by right. 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