proposition: Lemma nbet_cab : (bet' c' a' b') = false.
proof: Proof. rewrite /bet' /bet /betE /a /b /c !mxE /= !neq_mx. rewrite oner_eqm1 oppr_eq0 oner_eq0. have: betS 1%:M (-1)%:M 0%:M = false. move=>t. rewrite /betS /betR /ratio /=. case: pickP => /= [i|/all_v_neq0 H]. case: i => ? ?. rewrite ord1 !mxE mul0rn sub0r !mulr1n invrN mulrN divr1. by rewrite opprB ltr_subl_addr subrr 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