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

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

%proving nat2

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

two_def

 ⊢  

successor_in_nats

 ⊢  

one_plus_one__in__nats = successor_in_nats.instantiate({n:one})

one_plus_one__in__nats:  ⊢  

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

%qed

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

	step type	requirements	statement
0	instantiation	1, 2, 3*	⊢
	:
1	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.successor_in_nats
2	conjecture		⊢
	proveit.numbers.numerals.decimals.nat1
3	conjecture		⊢
	proveit.numbers.numerals.decimals.add_1_1
*equality replacement requirements