Efficient computation of (a - 1) % N

predModKR computes (a + (N - 1)) % N using Nat.rec so the kernel can reduce it via eagerReduce, avoiding the overhead of general modular arithmetic.

def predModKR (a N : Nat) : Nat

Kernel-reducible predecessor mod: computes (a + (N - 1)) % N for a ≤ N.

Equations

• predModKR a N = Nat.rec N.pred (fun (a x : Nat) => a) a

theorem predModKR_eq {a N : Nat} (hn : N ≠ 0) (ha : a ≤ N) : predModKR a N = (a + (N - 1)) % N