proposition: Lemma bet_abx_x00_eq0 (x': @Vector R 1): bet a' b' x' -> x' 0 0 = 0.
proof: Proof. rewrite /bet=> /orP[/betEP[[_ <-]|/eqP ab_eq |<- ] |/betSP[P1 k_gt0 k_lt1]]. by rewrite /b'!mxE /=. exfalso; move:ab_eq. by rewrite /a' /b' row2_eq [X in _ && X]eq_sym one_half_neq0 andbF. by rewrite /b'!mxE /=. move/eqP:P1. rewrite a'_eq0 !subr0 -subr_eq0 vector2_eq0 !mxE /= add0r oppr_eq0. move: k_gt0. rewrite lt0r mulf_eq0 a'_eq0=>/andP[/negPf -> _]. by rewrite orFb=>/andP[/eqP -> _]. 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