proposition: Lemma bet_abx_x01_gt (x': @Vector R 1): bet a' b' x'-> x'!=b' -> 1 / (1+1) < x' 0 1 .
proof: Proof. rewrite /bet=> /orP[/betEP[[_ <-]| /eqP ab_eq |<- ] |/betSP[]]. by rewrite eqxx. exfalso; move:ab_eq. by rewrite /a' /b' row2_eq [X in _ && X]eq_sym one_half_neq0 andbF. by rewrite eqxx. set k := betR a' b' x'. rewrite a'_eq0 !subr0. move=> b_kx k_gt0 k_lt1. have: k^-1 *: b' = x'. rewrite b_kx scalerA mulrC divff. by rewrite scale1r. move:k_gt0. by rewrite lt0r=>/andP[? ?]. move=><- _. rewrite !mxE /=. rewrite -[X in X < _]mul1r. rewrite -subr_lt0 -mulrBl. rewrite pmulr_llt0. by rewrite subr_lt0 invf_gt1. exact: one_half_gt0. 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