proposition: Lemma scalar_productZR (q r: Plane) (t: R): scalar_product q (t *: r) = t * scalar_product q r.
proof: Proof. by rewrite scalar_productC scalar_productZL scalar_productC. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)