proposition: Lemma val_ipred m (i : 'I_m) : ipred i = i.-1 :> nat.
proof: Proof. case: m i => [[]//|n i /=]. by rewrite modn_small // (leq_ltn_trans (leq_pred _) (ltn_ord i)). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)