Proof of proveit.numbers.number_sets.integers.nonneg_int_is_natural theorem

import proveit
from proveit import defaults
from proveit import a, m, n, x, A, B
from proveit.core_expr_types import A_1_to_m
from proveit.numbers import zero, num, Neg, NaturalPos, Integer, greater, Natural, greater_eq
from proveit.logic import NotInSet, SetOfAll, InSet, Implies, And
from proveit.logic.sets.unification import membership_unfolding
from proveit.numbers.number_sets.natural_numbers  import natural_pos_def
from proveit.numbers.number_sets.integers  import integers_def
theory = proveit.Theory() # the theorem's theory

%proving nonneg_int_is_natural

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
nonneg_int_is_natural:
(see dependencies)

nonneg_int_is_natural may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

# defaults.assumptions = nonneg_int_is_natural.conditions

# integers_def

# int_union = integers_def.expr.rhs

# int_union.operands

# membership_unfolding

# spec1 = membership_unfolding.instantiate({x:a, m:num(2), A:int_union.operands}, assumptions = [InSet(m, NaturalPos), *defaults.assumptions])

# a_in_int = defaults.assumptions[0]

# a_elem_union = Implies(And(a_in_int, integers_def.expr),InSet(a,int_union))

# new_assumpt = [defaults.assumptions]+ [integers_def.expr]