proposition: Lemma x_neq0 (x': @Vector R 1): bet a' b' x'-> x'!=b' -> x' != 0.
proof: Proof. move=> ? ?. rewrite vector2_neq0 [x' 0 1 != 0]lt0r_neq0 ?orbT //. apply lt_trans with (1/(1+1)). rewrite one_half_gt0 //. by apply bet_abx_x01_gt. 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