proposition: Lemma scalar_productrr_gt0 u : u != 0 -> 0 < scalar_product u u.
proof: Proof. move=>u0. rewrite lt0r; apply/andP; split; last by apply scalar_productrr_ge0. apply/negP; rewrite /scalar_product paddr_eq0. 2, 3: by apply sqr_ge0. rewrite 2!sqrf_eq0=>/andP[/eqP u10 /eqP u20]. by move: u0=>/negP; apply; rewrite -pair_eqE; apply/andP; split; apply/eqP. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)