Let x and y be given.
Assume Hx.
Apply Hx to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hk.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hxkm: x = eps_ k * m.
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim Lekm: SNo (eps_ k * m).
An exact proof term for the current goal is SNo_mul_SNo (eps_ k) m Lek Lm.
Assume Hy.
Apply Hy to the current goal.
Let l be given.
Assume H.
Apply H to the current goal.
Assume Hl: l ∈ ω.
We prove the intermediate claim Lel: SNo (eps_ l).
An exact proof term for the current goal is SNo_eps_ l Hl.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ int.
Assume Hyln: y = eps_ l * n.
We prove the intermediate claim Ln: SNo n.
An exact proof term for the current goal is int_SNo n Hn.
We prove the intermediate claim Leln: SNo (eps_ l * n).
An exact proof term for the current goal is SNo_mul_SNo (eps_ l) n Lel Ln.
We will prove ∃k' ∈ ω, ∃m' ∈ int, x + y = eps_ k' * m'.
We use (k + l) to witness the existential quantifier.
Apply andI to the current goal.
We will prove k + l ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega k Hk l Hl.
We use (2 ^ l * m + 2 ^ k * n) to witness the existential quantifier.
We prove the intermediate claim L2l: 2 ^ l ∈ int.
Apply Subq_omega_int to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 l (omega_nat_p l Hl).
We prove the intermediate claim L2lm: 2 ^ l * m ∈ int.
Apply int_mul_SNo to the current goal.
An exact proof term for the current goal is L2l.
An exact proof term for the current goal is Hm.
We prove the intermediate claim L2k: 2 ^ k ∈ int.
Apply Subq_omega_int to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 k (omega_nat_p k Hk).
We prove the intermediate claim L2kn: 2 ^ k * n ∈ int.
Apply int_mul_SNo to the current goal.
An exact proof term for the current goal is L2k.
An exact proof term for the current goal is Hn.
Apply andI to the current goal.
We will prove 2 ^ l * m + 2 ^ k * n ∈ int.
Apply int_add_SNo to the current goal.
An exact proof term for the current goal is L2lm.
An exact proof term for the current goal is L2kn.
We will prove x + y = eps_ (k + l) * (2 ^ l * m + 2 ^ k * n).
rewrite the current goal using mul_SNo_eps_eps_add_SNo k Hk l Hl (from right to left).
We will prove x + y = (eps_ k * eps_ l) * (2 ^ l * m + 2 ^ k * n).
rewrite the current goal using mul_SNo_distrL (eps_ k * eps_ l) (2 ^ l * m) (2 ^ k * n) (SNo_mul_SNo (eps_ k) (eps_ l) Lek Lel) (int_SNo (2 ^ l * m) L2lm) (int_SNo (2 ^ k * n) L2kn) (from left to right).
We will prove x + y = (eps_ k * eps_ l) * 2 ^ l * m + (eps_ k * eps_ l) * 2 ^ k * n.
Use f_equal.
We will prove x = (eps_ k * eps_ l) * 2 ^ l * m.
rewrite the current goal using mul_SNo_assoc (eps_ k) (eps_ l) (2 ^ l * m) Lek Lel (int_SNo (2 ^ l * m) L2lm) (from right to left).
We will prove x = eps_ k * eps_ l * 2 ^ l * m.
rewrite the current goal using mul_SNo_assoc (eps_ l) (2 ^ l) m Lel (int_SNo (2 ^ l) L2l) (int_SNo m Hm) (from left to right).
We will prove x = eps_ k * (eps_ l * 2 ^ l) * m.
rewrite the current goal using mul_SNo_eps_power_2 l (omega_nat_p l Hl) (from left to right).
We will prove x = eps_ k * 1 * m.
rewrite the current goal using mul_SNo_oneL m (int_SNo m Hm) (from left to right).
We will prove x = eps_ k * m.
An exact proof term for the current goal is Hxkm.
We will prove y = (eps_ k * eps_ l) * (2 ^ k * n).
rewrite the current goal using mul_SNo_com_4_inner_mid (eps_ k) (eps_ l) (2 ^ k) n Lek Lel (int_SNo (2 ^ k) L2k) (int_SNo n Hn) (from left to right).
We will prove y = (eps_ k * 2 ^ k) * (eps_ l * n).
rewrite the current goal using mul_SNo_eps_power_2 k (omega_nat_p k Hk) (from left to right).
We will prove y = 1 * (eps_ l * n).
rewrite the current goal using mul_SNo_oneL (eps_ l * n) Leln (from left to right).
An exact proof term for the current goal is Hyln.
∎