Let x, x', x'i, y and y' be given.
Assume Hx Hxpos Hx' Hx'i Hx'x'i Hy Hxy1 Hy' Hy'y.
Apply SepE (SNoL x) (λw ⇒ 0 < w) x' Hx' to the current goal.
Apply SNoL_E x Hx x' Hx'L to the current goal.
We prove the intermediate
claim Lxy:
SNo (x * y).
An
exact proof term for the current goal is
SNo_mul_SNo x y Hx Hy.
We prove the intermediate
claim Lxy':
SNo (x * y').
An
exact proof term for the current goal is
SNo_mul_SNo x y' Hx Hy'.
We prove the intermediate
claim L1:
1 + - x * y < 0.
We will
prove 1 < 0 + x * y.
rewrite the current goal using
add_SNo_0L (x * y) Lxy (from left to right).
An exact proof term for the current goal is Hxy1.
We prove the intermediate
claim L2:
(x' + - x) * x'i < 0.
We will
prove x' + - x < 0.
We will
prove x' < 0 + x.
rewrite the current goal using
add_SNo_0L x Hx (from left to right).
An exact proof term for the current goal is Hx'3.
An
exact proof term for the current goal is
SNo_recip_pos_pos x' x'i Hx'1 Hx'i Hx'pos Hx'x'i.
We prove the intermediate
claim L3:
0 < 1 + - x * y'.
rewrite the current goal using Hy'y (from left to right).
We will
prove 0 < (1 + - x * y) * (x' + - x) * x'i.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.
We will
prove x * y' < 1.
rewrite the current goal using
add_SNo_0L (x * y') Lxy' (from right to left).
We will
prove 0 + x * y' < 1.