proposition: Lemma cswapE_neq t i j k : k != i -> k != j -> tnth (cfun (cswap i j) t) k = tnth t k.
proof: Proof. move=> kDi kDj. rewrite tnth_map !ffunE tnth_ord_tuple. by rewrite (negPf kDi) (negPf kDj) leqnn minxx. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple