proposition: Lemma betR_abc : betR a' b' c' = 0.
proof: Proof. rewrite /betR /ratio. case: pickP => /= [x|/all_v_neq0 //]. rewrite /a' /b' /c' !mxE /=. case: x => [] [|[|[|//]]] //= p; rewrite !subr0 ?divr1 ?eqxx //. 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