proposition: Lemma triangle_ineq v w : norm(v + w) <= norm(v) + norm(w).
proof: Proof. case: (w =P 0). move ->. by rewrite {3}/norm mul0mx mxE sqrtr0 !addr0 lexx. move=>/eqP w_neq0. suffices : (norm (v + w))^+2 <= (norm v + norm w)^+2. rewrite -ler_sqrt ; last by rewrite addrC expr2 mulr_gt0 ?addr_ge_gt0 ?lt_def ?norm_ge0 // /norm lt0r_neq0 // sqrtr_gt0 lt_def quad_ge0 quad_neq0 w_neq0. by rewrite !sqrtr_sqr !ger0_norm ?addr_ge0 ?norm_ge0. rewrite norm_sqr mulmxDl ![_*m(v+w)^T]dotC !mulmxDl mxE. rewrite ![(_*m_^T+_*m_^T) 0 0]mxE expr2 mulrDr !mulrDl -!norm_sqr -!expr2. rewrite ?ler_add ?lexx //. by move: (cauchy_schwartz' w v) => /andP[_ ]. by move: (cauchy_schwartz' v w) => /andP[_ ]. 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