proposition: Lemma cauchy_schwartz v w : ((v *m w^T) 0 0)^+2 <= (v*m v^T) 0 0 * (w*m w^T) 0 0.
proof: Proof. case: ((w *m w^T) =P 0). move=>/eqP. rewrite quad_eq0=>/eqP ->. by rewrite linear0 !mulmx0 !mxE expr2 !mulr0 lexx. move=> /eqP; rewrite quad_eq0 => w_neq0. set r := (v *m (w)^T) 0 0/(w*m(w)^T) 0 0. suffices: 0 <= ((v - r *: w)*m(v - r *: w)^T) 0 0. rewrite mulmxBl ![_ *m (v - r *: w)^T]dotC !mulmxBl. rewrite [v*m (r *: w)^T]dotC -!scalemxAl [_*m(r*:w)^T]dotC -scalemxAl. rewrite scalerA mxE /= mxE /= opprB. have: ((r * r) *: (w *m w^T) - r *: (w *m v^T)) 0 0 == 0. rewrite mxE /= mxE /= [X in _ + X]mxE /= subr_eq0. rewrite {2}/r mulrA mulrAC -!mulrA divff ?quad_neq0 //. by rewrite [w *m v ^T]dotC /r !mxE /= !mulrA mulr1 eqxx. move=> /eqP ->. rewrite addr0 [X in _ +X]mxE subr_ge0 /r mxE. rewrite [w*m v^T]dotC mulrC mulrA -expr2 ler_pdivr_mulr //. by rewrite lt0r quad_ge0 quad_neq0 w_neq0. by rewrite quad_ge0. 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