proposition: Lemma rotateD (p q : Plane) : rotate (p + q) = rotate p + rotate q.
proof: Proof. rewrite /rotate; apply pair_equal_spec; split=>//=. by rewrite opprD. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)