proposition: Lemma val_inext m (i : 'I_m) : inext i = (if i == m.-1 :> nat then i : nat else i.+1) :> nat.
proof: Proof. case: m i => [[]//|n i /=]. have:= (ltn_ord i); rewrite ltnS leq_eqVlt. by case: eqP => [->|_] /= iLn; rewrite modn_small. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)