We prove the intermediate claim LPz: P z.
Apply IH z to the current goal.
An exact proof term for the current goal is Hz1.
An exact proof term for the current goal is Hu1.
An exact proof term for the current goal is Hz2.
An exact proof term for the current goal is H1.
Apply LPz to the current goal.
Assume H2: P1 z.
Apply H2 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume H2.
Apply H2 to the current goal.
Let w be given.
Assume H2.
Apply H2 to the current goal.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoL_E y Hy w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate
claim Lvw:
SNo (v * w).
An
exact proof term for the current goal is
SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate
claim L3:
z + v * w < u + v * w.
We will
prove v * y + x * w < u + v * w.
An exact proof term for the current goal is L1 v Hv w Hw.
We prove the intermediate
claim L4:
z < u.
An
exact proof term for the current goal is
SNoLt_tra u z u Hu1 Hz1 Hu1 Hz3 L4.
Assume H2: P2 z.
Apply H2 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume H2.
Apply H2 to the current goal.
Let w be given.
Assume H2.
Apply H2 to the current goal.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoR_E y Hy w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate
claim Lvw:
SNo (v * w).
An
exact proof term for the current goal is
SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate
claim L5:
z + v * w < u + v * w.
We will
prove v * y + x * w < u + v * w.
An exact proof term for the current goal is L2 v Hv w Hw.
We prove the intermediate
claim L6:
z < u.
An
exact proof term for the current goal is
SNoLt_tra u z u Hu1 Hz1 Hu1 Hz3 L6.