proposition: Lemma bet_adt: bet' a d t.
proof: Proof. rewrite /bet' /bet /betS /a /d /t /=. have: betR a' d' t' = 1/(1+1). rewrite /betR /ratio a'_eq0 /= subr0. case: pickP => /= [x|/all_v_neq0 H]. rewrite /t' /d' !mxE /=; case: x => [] [|[| //]] //= p; rewrite -quarter subr0 -!mulrA !mul1r divff ?mulr1 ?invr_eq0 ?add11_neq0 ?eqxx //. by exfalso; apply H; rewrite -a'_eq0 /a' /t' row2_eq one_half_neq0. move ->. rewrite one_half_lt1 one_half_gt0 /= /a' /d' /t' vector2_eq. rewrite !mxE /= !subr0 quarter eqxx. by rewrite 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