proposition: Lemma cauchy_schwartz' v w : - norm v * norm w <= (v *m w^T) 0 0 <= norm v * norm w.
proof: Proof. case: (v*m v^T =P 0). move=> /eqP ;rewrite quad_eq0 => /eqP->. by rewrite /norm !mul0mx !mxE /= !sqrtr0 oppr0 mul0r lexx. move=> /eqP; rewrite quad_eq0 => v_neq0. case: (w*m w^T =P 0). move=> /eqP ;rewrite quad_eq0 => /eqP->. by rewrite /norm linear0 !mulmx0 !mxE /= !sqrtr0 !mulr0 lexx. move=> /eqP; rewrite quad_eq0 => w_neq0. move: (cauchy_schwartz v w). rewrite -[_^+2 <= _]ler_sqrt. rewrite sqrtr_sqr ler_norml !sqrtrM !/norm. by rewrite -mulNr. by rewrite quad_ge0. by rewrite mulr_gt0 ?lt0r ?quad_ge0 ?quad_neq0 ?w_neq0 ?v_neq0. 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