proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat