proposition: Lemma p_scalar_lt1 v w : (v *m v^T) 0 0 < 1 -> (w *m w^T) 0 0 < 1 -> v != w -> ( v *m w^T) 0 0 < 1.
proof: Proof. move => v_in_disk w_in_disk ?. apply lt_trans with ( ((v *m v^T) 0 0 + (w *m w^T) 0 0)/(1+1)). rewrite ltr_pdivl_mulr ?addr_gt0 ?ltr01 //. rewrite mulrDr mulr1. assert (0 < ((v - w) *m (v - w)^T) 0 0). by rewrite lt_def quad_ge0 quad_neq0 subr_eq0 andbT. move: H. rewrite mulmxBl [X in X - _]dotC [X in _ - X]dotC !mulmxBl 2!mxE /=. rewrite addrC mxE /= !addrA [X in _+X]mxE subr_gt0 [X in -X+_]mxE. rewrite addrC opprD [X in _ - X]mxE opprK -addrCA addrC. by rewrite ltr_subr_addr dotC. rewrite ltr_pdivr_mulr ?addr_gt0 ?ltr01 //. by rewrite mulrDr mulr1 ltr_add. 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