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| == norm v * norm w = (v == r *: w).
proof: Proof. move => w_neq0. suffices: (`|(v *m w^T) 0 0| == norm v * norm w) = (((v *m w^T) 0 0)^+2 == ((v*m v^T) 0 0 * (w*m w^T)0 0)). move->. by apply cauchy_schwartz_eq. rewrite -[X in _ = X]eqr_sqrt ?sqr_ge0 ?mulr_ge0 ?quad_ge0 //. by rewrite sqrtr_sqr sqrtrM -!/(norm _) ?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