proposition: Lemma swapZ (p : Plane) (t : R) : swap (t *: p) = t *: swap p.
proof: Proof. by apply pair_equal_spec. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)