proposition: Lemma bet_abx_x01_lt1 (x: @Point R 1): bet a' b' (#x) -> (#x) 0 1 < 1.
proof: Proof. move=> bet_abx. have: ((#x) *m (#x)^T) 0 0 < 1 by destruct x. have: ((0<= (#x) 0 1) || ((#x) 0 1<= 0)) by rewrite le_total. move=>/orP[x01_ge0| x01_le0 _]. rewrite !mxE !big_ord_recr !big_ord0 !mxE /= add0r. suffices: (#x) 0 0 * (#x) 0 0 + (#x) 0 1 * (#x) 0 1 = # x 0 (widen_ord (leqnSn 1) ord_max) * # x 0 (widen_ord (leqnSn 1) ord_max) + # x 0 ord_max * # x 0 ord_max. move=><-. by rewrite bet_abx_x00_eq0 // mulr0 add0r -expr2 expr_lt1. by congr ((#x) 0 _ * (#x) 0 _ + (#x) 0 _ * (#x) 0 _); apply val_inj. apply le_lt_trans with 0; rewrite ?ltr01 //. 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