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 SNoR_E x Hx x' Hx' to the current goal.
Assume Hx'1: SNo x'.
Assume Hx'2: SNoLev x' ∈ SNoLev x.
Assume Hx'3: x < x'.
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 Lx'pos: 0 < x'.
An exact proof term for the current goal is SNoLt_tra 0 x x' SNo_0 Hx Hx'1 Hxpos Hx'3.
We prove the intermediate claim L1: 1 + - x * y < 0.
Apply add_SNo_minus_Lt1b 1 (x * y) 0 SNo_1 Lxy SNo_0 to the current goal.
We will prove 1 < 0 + x * y.
rewrite the current goal using add_SNo_0L (x * y) Lxy (from left to right).
We will prove 1 < x * y.
An exact proof term for the current goal is Hxy1.
We prove the intermediate claim L2: 0 < (x' + - x) * x'i.
Apply mul_SNo_pos_pos (x' + - x) x'i (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hx'i to the current goal.
We will prove 0 < x' + - x.
Apply add_SNo_minus_Lt2b x' x 0 Hx'1 Hx SNo_0 to the current goal.
We will prove 0 + x < 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.
We will prove 0 < x'i.
An exact proof term for the current goal is SNo_recip_pos_pos x' x'i Hx'1 Hx'i Lx'pos Hx'x'i.
We prove the intermediate claim L3: 1 + - x * y' < 0.
rewrite the current goal using Hy'y (from left to right).
We will prove (1 + - x * y) * (x' + - x) * x'i < 0.
Apply mul_SNo_neg_pos (1 + - x * y) ((x' + - x) * x'i) (SNo_add_SNo 1 (- x * y) SNo_1 (SNo_minus_SNo (x * y) Lxy)) (SNo_mul_SNo (x' + - x) x'i (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hx'i) to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.
We will prove 1 < x * y'.
rewrite the current goal using add_SNo_0L (x * y') Lxy' (from right to left).
We will prove 1 < 0 + x * y'.
An exact proof term for the current goal is add_SNo_minus_Lt1 1 (x * y') 0 SNo_1 Lxy' SNo_0 L3.
∎