proposition: Lemma nbet_abc : (bet' a' b' c') = false.
proof: Proof. rewrite /bet' /bet /betE /a /b /c !mxE /= !neq_mx oner_eq0. rewrite [0 == 1]eq_sym oner_eq0. have: (betS 0%:M 1%:M 0%:M = false). rewrite /betS /betR /ratio /= => t. case: pickP => /= [i|/all_v_neq0 H]. case: i => ? ?. rewrite ord1 /= subrr. rewrite !mxE /=. by rewrite eqxx. by rewrite ltxx /= andbF. by move->;apply /andP; move=> [_ /orP[/or3P[||]|]]. 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