proposition: Lemma scalar_productC (p q: Plane): scalar_product p q = scalar_product q p.
proof: Proof. by rewrite /scalar_product /= [p.1*_]mulrC [p.2*_]mulrC. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)