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.
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.
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.
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.
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.
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 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.
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 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.
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.
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.