proposition: Lemma cfun_eswap n (t : n.-tuple A) : cfun ceswap t = [tuple if odd i then max (tnth t i) (tnth t (ipred i)) else min (tnth t i) (tnth t (inext i)) | i < n].
proof: Proof. apply: eq_from_tnth => i /=. rewrite /ceswap /cfun /=. rewrite !tnth_map /= !tnth_ord_tuple !ffunE. have [iO|iE] := boolP (odd i); last by rewrite ifT // val_inext; case: eqP. case: leqP => [iLip|] //. suff -> : ipred i = i by rewrite maxxx minxx. apply/val_eqP =>> /=; move: iLip; rewrite !val_ipred /=. by case: (i : nat) => //= i1; rewrite ltnn. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort