Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
We prove the intermediate
claim Lmn1:
m + n ∈ ω.
We prove the intermediate
claim Lmn2:
nat_p (m + n).
An
exact proof term for the current goal is
omega_nat_p (m + n) Lmn1.
We prove the intermediate
claim Lem:
SNo (eps_ m).
An
exact proof term for the current goal is
SNo_eps_ m Hm.
We prove the intermediate
claim Len:
SNo (eps_ n).
An
exact proof term for the current goal is
SNo_eps_ n Hn.
We prove the intermediate
claim Lemen:
SNo (eps_ m * eps_ n).
We prove the intermediate
claim Lemn:
SNo (eps_ (m + n)).
An
exact proof term for the current goal is
SNo_eps_ (m + n) Lmn1.
We prove the intermediate
claim L2m:
SNo (2 ^ m).
We prove the intermediate
claim L2n:
SNo (2 ^ n).
We will
prove SNo (2 ^ (m + n)).
We will
prove 2 ^ (m + n) ≠ 0.
rewrite the current goal using H1 (from right to left) at position 2.
We will
prove 0 < 2 ^ (m + n).
An exact proof term for the current goal is Lemen.
An exact proof term for the current goal is Lemn.
Use f_equal.
Use symmetry.
∎