proposition: Lemma scalar_productrr_ge0 p : 0 <= (scalar_product p p).
proof: Proof. by rewrite /scalar_product; apply addr_ge0; apply sqr_ge0. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)