proposition: Lemma cswapE_max t (i j : 'I_m) : tnth (cfun (cswap i j) t) j = max (tnth t i) (tnth t j).
proof: Proof. rewrite tnth_map !ffunE tnth_ord_tuple eqxx /=. case: (j =P i) => [->|/val_eqP /= jDi]; first by rewrite leqnn ltnn minxx maxxx. by rewrite leq_eqVlt (negPf jDi) /=; case: leqP; rewrite maxC. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple