proposition: Lemma rotate_rotate (p : Plane) : rotate (rotate p) = -p.
proof: Proof. by case p=>a b; apply pair_equal_spec; split=>//. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)