proveit.logic.sets.inclusion.superset_membership_from_proper_subset
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat