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 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 L3:
u + v * w < z + v * w.
We will
prove u + v * w < v * y + x * w.
An exact proof term for the current goal is L1 v Hv w Hw.
An exact proof term for the current goal is Hvw.
We prove the intermediate
claim L4:
u < z.
An
exact proof term for the current goal is
SNoLt_tra u z u Hu1 Hz1 Hu1 L4 Hz3.
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 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 L5:
u + v * w < z + v * w.
We will
prove u + v * w < v * y + x * w.
An exact proof term for the current goal is L2 v Hv w Hw.
An exact proof term for the current goal is Hvw.
We prove the intermediate
claim L6:
u < z.
An
exact proof term for the current goal is
SNoLt_tra u z u Hu1 Hz1 Hu1 L6 Hz3.