proposition: Lemma val_iadd m (i : 'I_m) k : iadd k i = (if k + i < m then k + i else i) :> nat.
proof: Proof. case: m i => [[]//|n i /=]; have iLn := ltn_ord i. by rewrite modn_small ?ltnS //=; case: (leqP (k + i)). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)