proposition: Lemma betR_cab : betR c' a' b' = 0 \/ betR c' a' b' = 1.
proof: Proof. rewrite /betR /ratio a_eq0 sub0r; case: pickP => /= [x| //]; last tauto. rewrite /b' /c' !mxE /=; case: x => [] [|[|[| //]]] //= p; rewrite ?subr0 ?eqxx // ?sub0r ?divff ?divr1 ?oppr0 ?oppr_eq0 ?oner_eq0; tauto. 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