proposition: Lemma scalar_product_swap (p q : Plane) : scalar_product (swap p) (swap q) = scalar_product p q.
proof: Proof. by rewrite swap_sym swap_swap. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)