proposition: Lemma swap_inj : injective swap.
proof: Proof. by move=>p q /(f_equal swap); rewrite 2!swap_swap. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)