proposition: Lemma clink_odd_jump_proof m k : [forall i : 'I_m, clink_odd_jump _ k (clink_odd_jump _ k i) == i].
proof: Proof. rewrite /clink_odd_jump. have [/= kO|kI] := boolP (odd k); apply/forallP => i /=; apply/eqP/val_eqP; rewrite !ffunE //. have m_gt0 : 0 < m by apply: leq_ltn_trans (ltn_ord i). have [/= iO|iE] := boolP (odd i); rewrite ?(val_iadd, val_isub) /=. case: ltnP => [kiLm|mLki]; last first. by rewrite iO !val_iadd [k + i < m]ltnNge mLki /= [k + i < m]ltnNge mLki. by rewrite oddD iO kO /= ?(val_iadd, val_isub) /= kiLm leq_addr addnC addnK. case: leqP => [kLi|iLk]; last first. by rewrite (negPf iE) !val_isub [k <= i]leqNgt iLk /= [k <= i]leqNgt iLk. rewrite oddB // (negPf iE) kO /= ?(val_iadd, val_isub) /= kLi. by rewrite addnC subnK // ifT. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple