proposition: Lemma bet_on_abscissa a b c : a <> b -> a 0 1 = 0 -> b 0 1 = 0 -> bet a b c -> c 0 1 = 0.
proof: Proof. rewrite /bet' /bet /betE; case: (a =P b)=> [//|_ /=]. case: (b =P c)=> [-> //|bc_neq /=]=> ab_neq Ha1 Hb1 /betSP'[_ Hc1 r_neq0 _]. move/eqP: Hc1; rewrite Ha1 Hb1 !subr0 eq_sym mulf_eq0=> /orP[/eqP Hr|/eqP-> //]. by move: r_neq0; rewrite Hr lt_def 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.Axioms.gupta_inspired_variant_axioms GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence