proposition: Lemma bet_bdc: bet' b d c.
proof: Proof. rewrite /bet' /bet /betS /b /c /d. have: betR b' d' c' == 1/(1+1). rewrite /betR /ratio /=. case: pickP => /= [x|/all_v_neq0 H]. rewrite /b' /c' /d' !mxE /=; case: x => [] [|[| //]] //= p; rewrite -quarter ?subr0 ?sub0r. rewrite !mul1r -!mulrA divff ?mulr1 ?invr_eq0 add11_neq0 //. rewrite invrN mulrN mulrBl divff; last by rewrite mul1r invr_neq0 ?add11_neq0. rewrite opprB. rewrite mul1r mulrAC divff; last by rewrite invr_neq0 ?add11_neq0. rewrite subr_eq. rewrite -[X in _==X+_]mul1r. rewrite addf_divrr ?divff ?eqxx ?add11_neq0 //. by exfalso; apply H; rewrite /c' /b' subr_eq0 row2_eq one_half_neq0 eq_sym one_half_neq0. move /eqP ->. rewrite one_half_lt1 one_half_gt0 /= /b' /c' /d' vector2_eq. rewrite !mxE /= !subr0 !sub0r quarter eqxx. rewrite -quarter -subr_eq0 mulrN opprK addrC !addrA. rewrite -mulrDl addf_div ?add11_neq0 //. rewrite !mul1r [((1 + 1) * (1 + 1))]mulrDl !mul1r. rewrite divff; last by rewrite lt0r_neq0 ?addr_gt0 ?ltr01. by rewrite mul1r subrr eqxx orbT. 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 algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence