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