Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
We prove the intermediate claim Lmn1: m + n ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega m Hm n Hn.
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).
An exact proof term for the current goal is SNo_mul_SNo (eps_ m) (eps_ n) Lem Len.
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).
An exact proof term for the current goal is SNo_exp_SNo_nat 2 SNo_2 m (omega_nat_p m Hm).
We prove the intermediate claim L2n: SNo (2 ^ n).
An exact proof term for the current goal is SNo_exp_SNo_nat 2 SNo_2 n (omega_nat_p n Hn).
Apply mul_SNo_nonzero_cancel (2 ^ (m + n)) to the current goal.
We will prove SNo (2 ^ (m + n)).
An exact proof term for the current goal is SNo_exp_SNo_nat 2 SNo_2 (m + n) Lmn2.
We will prove 2 ^ (m + n) ≠ 0.
Assume H1: 2 ^ (m + n) = 0.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 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 exp_SNo_nat_pos 2 SNo_2 SNoLt_0_2 (m + n) Lmn2.
We will prove SNo (eps_ m * eps_ n).
An exact proof term for the current goal is Lemen.
We will prove SNo (eps_ (m + n)).
An exact proof term for the current goal is Lemn.
We will prove 2 ^ (m + n) * (eps_ m * eps_ n) = 2 ^ (m + n) * eps_ (m + n).
Use transitivity with (2 ^ m * 2 ^ n) * (eps_ m * eps_ n), 2 ^ m * (2 ^ n * (eps_ m * eps_ n)), 2 ^ m * eps_ m, and 1.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is exp_SNo_nat_mul_add' 2 SNo_2 m Hm n Hn.
Use symmetry.
An exact proof term for the current goal is mul_SNo_assoc (2 ^ m) (2 ^ n) (eps_ m * eps_ n) L2m L2n (SNo_mul_SNo (eps_ m) (eps_ n) Lem Len).
Use f_equal.
We will prove 2 ^ n * (eps_ m * eps_ n) = eps_ m.
Use transitivity with (2 ^ n * eps_ n) * eps_ m, and 1 * eps_ m.
rewrite the current goal using mul_SNo_com (eps_ m) (eps_ n) Lem Len (from left to right).
An exact proof term for the current goal is mul_SNo_assoc (2 ^ n) (eps_ n) (eps_ m) L2n Len Lem.
Use f_equal.
An exact proof term for the current goal is mul_SNo_eps_power_2' n (omega_nat_p n Hn).
An exact proof term for the current goal is mul_SNo_oneL (eps_ m) Lem.
We will prove 2 ^ m * eps_ m = 1.
An exact proof term for the current goal is mul_SNo_eps_power_2' m (omega_nat_p m Hm).
Use symmetry.
We will prove 2 ^ (m + n) * eps_ (m + n) = 1.
An exact proof term for the current goal is mul_SNo_eps_power_2' (m + n) Lmn2.
∎