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