proposition: Lemma cauchy_schwartz_eq v w (r := ((v *m w^T) 0 0)/((w *m w^T) 0 0)): w != 0 -> (((v *m w^T) 0 0)^+2 == ((v*m v^T) 0 0 * (w*m w^T)0 0)) = (v == r *: w).
proof: Proof. move=> w_neq0. apply /eqP /eqP. move=> H. suffices: (((v - r *: w) *m (v - r *: w)^T) == 0). by rewrite quad_eq0 subr_eq0 => /eqP. rewrite [X in X == 0]mx11_scalar. rewrite mulmxBl ![_ *m (v-r*:w)^T]dotC !mulmxBl. rewrite -!scalemxAl ![_*m(r*:w)^T]dotC -!scalemxAl scalerA. rewrite opprB mxE /=. 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 mxE /= [X in _ + X]mxE /=. rewrite /r [ X in _ - X]mxE /= [w*m(v)^T]dotC. rewrite mulrAC -expr2 H -mulrA divff ?quad_neq0 //. rewrite mulr1 subrr. by rewrite [X in _ == X]mx11_scalar !mxE /=. move->. rewrite -scalemxAl mxE /= expr2. rewrite -scalemxAl [_*m(r*:w)^T]dotC -scalemxAl scalerA. rewrite [((r * r) *: (w *m w^T)) 0 0]mxE /=. by rewrite mulrAC !mulrA. 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