Basic lemmas about natural numbers #
The primary purpose of the lemmas in this file is to assist with reasoning about sizes of objects, array indices and such.
This file was upstreamed from Std, and later these lemmas should be organised into other files more systematically.
See forall_lt_succ_right'
for a variant where p
takes the bound as an argument.
add #
sub #
@[reducible, inline]