State an axiom for the maximum integer value being smaller than the field prime

[iamrecursion]

Currently Lampe plays quite loosely with the valid sizes for both signed and unsigned integers. We have it directly from Aztec that they restrict the maximum integer size $M$ such that $2^M < p$, the field prime. We should probably have some axiom representing this fact in Lampe.

[iamrecursion]

While this was partially handled by the addition of the ability to predicate theorems on having at least 'n' bits in their field, this is not entirely complete.

We should change the definition of the .i and .u integers to ensure that no number of bits N can be created that exceeds the number of bits available in the field.