proposition: Lemma cfun_odd_jump n k (t : n.-tuple A) : odd k -> cfun (codd_jump k) t = [tuple if odd i then min (tnth t i) (tnth t (iadd k i)) else max (tnth t i) (tnth t (isub k i)) | i < n].
proof: Proof. move=> kO; apply: eq_from_tnth => i /=. rewrite /codd_jump /cfun /=. rewrite !tnth_map /= !tnth_ord_tuple. rewrite /clink_odd_jump kO !ffunE. have [iO|iE] := boolP (odd i). by rewrite ifT // val_iadd; case: ltnP => // *; apply: leq_addl. rewrite val_isub; case: (leqP k) => [kLi|iLk]; last first. suff -> : isub k i = i by rewrite minxx maxxx if_same. by apply/val_eqP; rewrite /= val_isub leqNgt iLk. rewrite ifN // -ltnNge ltn_subLR //. by case: (k) kO => // k1 _; rewrite addSn ltnS leq_addl. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple