Proof of proveit.numbers.ordering.max_nat_n_zero_is_n theorem¶
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import n, x, y, defaults
from proveit.numbers import zero
from proveit.numbers.ordering import max_def_bin
In [2]:
%proving max_nat_n_zero_is_n
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
max_nat_n_zero_is_n:
(see dependencies)
max_nat_n_zero_is_n:
(see dependencies)
In [3]:
defaults.assumptions = max_nat_n_zero_is_n.conditions
defaults.assumptions: 
In [4]:
max_def_bin
In the following instantiation, we need to set auto_simplify=False, else we over-simplify and end up with the unhelpful $n = n$:
In [ ]:
In [5]:
max_def_bin_inst = max_def_bin.instantiate({x: n, y: zero}, auto_simplify=False)
max_def_bin_inst: 
⊢ 
⊢ 
Prove-It can then complete the formal proof on its own, but it's nice to explicitly show the final step before handing it off to Prove-It:
In [ ]:
In [6]:
max_def_bin_inst.inner_expr().rhs.simplify()
In [7]:
%qed
Out[7]:
