# Proof of proveit.numbers.numerals.decimals.nat2 theorem¶

In [1]:
import proveit
from proveit import n
from proveit.numbers import zero, one, two, Add
from proveit.numbers.numerals.decimals  import two_def
from proveit.numbers.number_sets.natural_numbers  import zero_in_nats, successor_in_nats
theory = proveit.Theory() # the theorem's theory

# testing
from proveit.numbers.numerals.decimals import tuple_len_2

In [2]:
%proving nat2

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
nat2:
(see dependencies)
In [3]:
two_def

In [4]:
successor_in_nats

In [5]:
one_plus_one__in__nats = successor_in_nats.instantiate({n:one})

one_plus_one__in__nats:
nat2 has been proven.  Now simply execute "%qed".

In [6]:
%qed

proveit.numbers.numerals.decimals.nat2 has been proven.

Out[6]:
step typerequirementsstatement
0instantiation1, 2, 3*
:
1axiom
proveit.numbers.number_sets.natural_numbers.successor_in_nats
2conjecture
proveit.numbers.numerals.decimals.nat1
3conjecture