proposition: Lemma clink_eswap_proof m : [forall i : 'I_m, clink_eswap _ (clink_eswap _ i) == i].
proof: Proof. 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_inext, val_ipred) /=. case: (ltngtP i 0) => // [o_gt0 | iE]; last by rewrite iE in iO. rewrite -[odd _]negbK -oddS prednK // iO val_inext val_ipred. rewrite -[i.-1 == _]eqSS !prednK //. by rewrite [(i : nat) == m]eqn_leq [m <= _]leqNgt ltn_ord andbF. have [iE1 | /eqP iD] := (i : nat) =P m.-1. by rewrite (negPf iE) !val_inext /= iE1 !eqxx. by rewrite oddS (negPf iE) /= /= val_ipred /= val_inext /= (negPf iD). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort