proveit.numbers.number_sets.integers.nonpos_int_within_int