proposition: Lemma val_isub m (i : 'I_m) k : isub k i = (if k <= i then i - k else i) :> nat.
proof: Proof. case: m i => [[]//|n i /=]; have iLn := ltn_ord i. rewrite modn_small //=; case: (leqP k) => // _. apply: leq_ltn_trans _ iLn. by rewrite -[X in _ <= X]subn0 leq_sub. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)