Proof of proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos theorem

import proveit
from proveit import defaults
from proveit import a, b, n
from proveit.numbers import zero, one, greater, greater_eq
theory = proveit.Theory() # the theorem's theory

%proving nonzero_if_is_nat_pos

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

defaults.assumptions = nonzero_if_is_nat_pos.conditions

defaults.assumptions:

greater(n, zero).conclude_via_transitivity()

 ⊢  

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

%qed

proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , :
2	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
3	instantiation	4, 5, 6, 7	⊢
	: , :
4	conjecture		⊢
	proveit.numbers.ordering.less_is_not_eq_nat
5	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
6	instantiation	8, 9, 14	⊢
	: , : , :
7	instantiation	10, 11, 12	⊢
	: , : , :
8	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
9	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
10	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
11	conjecture		⊢
	proveit.numbers.numerals.decimals.less_0_1
12	instantiation	13, 14	⊢
	:
13	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
14	assumption		⊢