proposition: Lemma col_2D_bet' a b c : (a 0 0 - b 0 0) * (b 0 1 - c 0 1) == (a 0 1 - b 0 1) * (b 0 0 - c 0 0) -> (bet' a b c \/ bet' b c a \/ bet' c a b).
proof: Proof. rewrite /bet'; case: (a =P b)=> [E1|?]; case: (b =P c)=> [E2|NE]; case: (c =P a)=> [E3|?]; rewrite ?E1 ?E2 ?E3 ?bet_xxa ?bet_axx ?bet_xax ?eqxx; rewrite ?andbT ?andbF; try solve[intuition; by []]; rewrite /=; try solve[exfalso; apply NE; by rewrite E3 E1]; case: (a 0 1 =P 0)=> _ /=; try solve [intuition; by []]; apply col_2D. 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.Axioms.gupta_inspired_variant_axioms GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence