In [1]:
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
In [2]:
%proving posnat1
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
(see dependencies)
posnat1 may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [3]:
In [4]:
one_in_natural = InSet(one, Natural).prove()
one_in_natural:  ⊢  
In [5]:
greater(one, zero).prove()
In [6]:
# %qed