Proof of proveit.numbers.numerals.decimals.posnat1 theorem

import proveit
from proveit import n
from proveit.numbers import zero, one, greater
from proveit.numbers import Natural, NaturalPos
from proveit.numbers.number_sets.natural_numbers  import natural_pos_def
from proveit.logic import InSet
theory = proveit.Theory() # the theorem's theory

%proving posnat1

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

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

natural_pos_def

 ⊢  

one_in_natural = InSet(one, Natural).prove()

one_in_natural:  ⊢  

greater(one, zero).prove()

 ⊢  

# %qed