proposition: Lemma nbet_bca : (bet' b' c' a') = false.
proof: Proof. rewrite /bet'/bet /betE /a /b /c !mxE /= !neq_mx. rewrite oner_eq0 [0 == 1]eq_sym oner_eq0. rewrite gt_eqF ?gt0_cp ?ltr01 //. have: betS 0%:M 1%:M (-1)%:M = false. move=>t. rewrite /betS /betR /ratio. case: pickP => /= [i|/all_v_neq0 H]. case: i => ? ?. rewrite ord1 !mxE /= mul0rn subr0 mulr1n subr0 invrN mulrN. rewrite divff ?oner_eq0 //. by rewrite oppr_gt0 ltr10 andbF. 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