proposition: Lemma cswapE_min t (i j : 'I_m) : tnth (cfun (cswap i j) t) i = min (tnth t i) (tnth t j).
proof: Proof. by rewrite tnth_map !ffunE tnth_ord_tuple /= eqxx; case: leqP. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple