proposition: Lemma clink_swap_proof (i j : 'I_m) : [forall k, clink_swap i j (clink_swap i j k) == k].
proof: Proof. apply/forallP => /= x. rewrite !ffunE; case: (x =P i) => [->|/eqP xDi]; rewrite ?eqxx. by case: (j =P i) => [->|] //. by case: (x =P j) => [->|/eqP xDj]; rewrite ?(negPf xDi, negPf xDj) !eqxx. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple