This ensures that simp succeeds on pred (n + 1) = n.

A natural number m divides the sum m + n if and only if m divides b.

A natural number m divides the sum n + m if and only if m divides b.

Partial predecessor operation. Returns ppred n = some m if n = m + 1, otherwise none.

Partial subtraction operation. Returns psub m n = some k if m = n + k, otherwise none.

fact n is the factorial of n.

choose n 2 is the n-th triangle number.

find_greatest P b is the largest i ≤ bound such that P i holds, or 0 if no such i exists