proveit.logic.sets.inclusion.superset_membership_from_proper_subset
proveit.numbers.numerals.decimals.add_1_1
proveit.numbers.numerals.decimals.nat1