proposition: Lemma swap_swap (p : Plane) : swap (swap p) = p.
proof: Proof. by rewrite /swap/=; apply/esym; apply surjective_pairing. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)