succ package:natural-arithmetic

Return the successor of the Fin or return nothing if the argument is the greatest inhabitant.

The successor of a number.

Variant of succ for unlifted finite numbers.

Unlifted variant of succ.

Weaken a strict inequality to a non-strict inequality, incrementing the right-hand argument by one.