proposition: Lemma scalar_productDr (p q r : Plane): scalar_product r (p + q) = scalar_product r p + scalar_product r q.
proof: Proof. by rewrite scalar_productC scalar_productDl; congr add; apply scalar_productC. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)