Let x and y be given.
Assume Hx Hy.
Let p be given.
Assume Hp.
Apply mul_SNo_eq_2 x y Hx Hy to the current goal.
Let L and R be given.
Assume HLE HLI1 HLI2 HRE HRI1 HRI2 He.
Apply mul_SNo_prop_1 x Hx y Hy to the current goal.
Assume Hxy: SNo (x * y).
Assume Hxy1: ∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v.
Assume Hxy2: ∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v.
Assume Hxy3: ∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v.
Assume Hxy4: ∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v.
We prove the intermediate claim LLR: SNoCutP L R.
We will prove (∀w ∈ L, SNo w) ∧ (∀z ∈ R, SNo z) ∧ (∀w ∈ L, ∀z ∈ R, w < z).
Apply and3I to the current goal.
Let w be given.
Assume Hw.
We will prove SNo w.
Apply HLE w Hw to the current goal.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv Hwe.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using Hwe (from left to right).
We will prove SNo (u * y + x * v + - u * v).
Apply SNo_mul_SNo_lem to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hua.
An exact proof term for the current goal is Hva.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv Hwe.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using Hwe (from left to right).
We will prove SNo (u * y + x * v + - u * v).
Apply SNo_mul_SNo_lem to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hua.
An exact proof term for the current goal is Hva.
Let z be given.
Assume Hz.
We will prove SNo z.
Apply HRE z Hz to the current goal.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv Hze.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using Hze (from left to right).
We will prove SNo (u * y + x * v + - u * v).
Apply SNo_mul_SNo_lem to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hua.
An exact proof term for the current goal is Hva.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv Hze.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using Hze (from left to right).
We will prove SNo (u * y + x * v + - u * v).
Apply SNo_mul_SNo_lem to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hua.
An exact proof term for the current goal is Hva.
Let w be given.
Assume Hw.
Let z be given.
Assume Hz.
We will prove w < z.
Apply HLE w Hw to the current goal.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv Hwe.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hua: SNo u.
Assume _ _.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva: SNo v.
Assume _ _.
We prove the intermediate claim Luy: SNo (u * y).
An exact proof term for the current goal is SNo_mul_SNo u y Hua Hy.
We prove the intermediate claim Lxv: SNo (x * v).
An exact proof term for the current goal is SNo_mul_SNo x v Hx Hva.
We prove the intermediate claim Luv: SNo (u * v).
An exact proof term for the current goal is SNo_mul_SNo u v Hua Hva.
Apply HRE z Hz to the current goal.
Let u' be given.
Assume Hu'.
Let v' be given.
Assume Hv' Hze.
Apply SNoL_E x Hx u' Hu' to the current goal.
Assume Hu'a: SNo u'.
Assume _ _.
Apply SNoR_E y Hy v' Hv' to the current goal.
Assume Hv'a: SNo v'.
Assume _ _.
We prove the intermediate claim Lu'y: SNo (u' * y).
An exact proof term for the current goal is SNo_mul_SNo u' y Hu'a Hy.
We prove the intermediate claim Lxv': SNo (x * v').
An exact proof term for the current goal is SNo_mul_SNo x v' Hx Hv'a.
We prove the intermediate claim Lu'v': SNo (u' * v').
An exact proof term for the current goal is SNo_mul_SNo u' v' Hu'a Hv'a.
rewrite the current goal using Hwe (from left to right).
rewrite the current goal using Hze (from left to right).
We will prove u * y + x * v + - u * v < u' * y + x * v' + - u' * v'.
Apply add_SNo_minus_Lt_lem (u * y) (x * v) (u * v) (u' * y) (x * v') (u' * v') Luy Lxv Luv Lu'y Lxv' Lu'v' to the current goal.
We will prove u * y + x * v + u' * v' < u' * y + x * v' + u * v.
Apply SNoLt_tra (u * y + x * v + u' * v') (x * y + u * v + u' * v') (u' * y + x * v' + u * v) (SNo_add_SNo_3 (u * y) (x * v) (u' * v') Luy Lxv Lu'v') (SNo_add_SNo_3 (x * y) (u * v) (u' * v') Hxy Luv Lu'v') (SNo_add_SNo_3 (u' * y) (x * v') (u * v) Lu'y Lxv' Luv) to the current goal.
We will prove u * y + x * v + u' * v' < x * y + u * v + u' * v'.
Apply add_SNo_3_3_3_Lt1 (u * y) (x * v) (x * y) (u * v) (u' * v') Luy Lxv Hxy Luv Lu'v' to the current goal.
We will prove u * y + x * v < x * y + u * v.
An exact proof term for the current goal is Hxy1 u Hu v Hv.
We will prove x * y + u * v + u' * v' < u' * y + x * v' + u * v.
Apply add_SNo_3_2_3_Lt1 (x * y) (u' * v') (u' * y) (x * v') (u * v) Hxy Lu'v' Lu'y Lxv' Luv to the current goal.
We will prove u' * v' + x * y < u' * y + x * v'.
rewrite the current goal using add_SNo_com (u' * v') (x * y) Lu'v' Hxy (from left to right).
An exact proof term for the current goal is Hxy3 u' Hu' v' Hv'.
Let u' be given.
Assume Hu'.
Let v' be given.
Assume Hv' Hze.
Apply SNoR_E x Hx u' Hu' to the current goal.
Assume Hu'a: SNo u'.
Assume _ _.
Apply SNoL_E y Hy v' Hv' to the current goal.
Assume Hv'a: SNo v'.
Assume _ _.
We prove the intermediate claim Lu'y: SNo (u' * y).
An exact proof term for the current goal is SNo_mul_SNo u' y Hu'a Hy.
We prove the intermediate claim Lxv': SNo (x * v').
An exact proof term for the current goal is SNo_mul_SNo x v' Hx Hv'a.
We prove the intermediate claim Lu'v': SNo (u' * v').
An exact proof term for the current goal is SNo_mul_SNo u' v' Hu'a Hv'a.
rewrite the current goal using Hwe (from left to right).
rewrite the current goal using Hze (from left to right).
We will prove u * y + x * v + - u * v < u' * y + x * v' + - u' * v'.
Apply add_SNo_minus_Lt_lem (u * y) (x * v) (u * v) (u' * y) (x * v') (u' * v') Luy Lxv Luv Lu'y Lxv' Lu'v' to the current goal.
We will prove u * y + x * v + u' * v' < u' * y + x * v' + u * v.
Apply SNoLt_tra (u * y + x * v + u' * v') (x * y + u * v + u' * v') (u' * y + x * v' + u * v) (SNo_add_SNo_3 (u * y) (x * v) (u' * v') Luy Lxv Lu'v') (SNo_add_SNo_3 (x * y) (u * v) (u' * v') Hxy Luv Lu'v') (SNo_add_SNo_3 (u' * y) (x * v') (u * v) Lu'y Lxv' Luv) to the current goal.
We will prove u * y + x * v + u' * v' < x * y + u * v + u' * v'.
Apply add_SNo_3_3_3_Lt1 (u * y) (x * v) (x * y) (u * v) (u' * v') Luy Lxv Hxy Luv Lu'v' to the current goal.
We will prove u * y + x * v < x * y + u * v.
An exact proof term for the current goal is Hxy1 u Hu v Hv.
We will prove x * y + u * v + u' * v' < u' * y + x * v' + u * v.
Apply add_SNo_3_2_3_Lt1 (x * y) (u' * v') (u' * y) (x * v') (u * v) Hxy Lu'v' Lu'y Lxv' Luv to the current goal.
We will prove u' * v' + x * y < u' * y + x * v'.
rewrite the current goal using add_SNo_com (u' * v') (x * y) Lu'v' Hxy (from left to right).
An exact proof term for the current goal is Hxy4 u' Hu' v' Hv'.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv Hwe.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hua: SNo u.
Assume _ _.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva: SNo v.
Assume _ _.
We prove the intermediate claim Luy: SNo (u * y).
An exact proof term for the current goal is SNo_mul_SNo u y Hua Hy.
We prove the intermediate claim Lxv: SNo (x * v).
An exact proof term for the current goal is SNo_mul_SNo x v Hx Hva.
We prove the intermediate claim Luv: SNo (u * v).
An exact proof term for the current goal is SNo_mul_SNo u v Hua Hva.
Apply HRE z Hz to the current goal.
Let u' be given.
Assume Hu'.
Let v' be given.
Assume Hv' Hze.
Apply SNoL_E x Hx u' Hu' to the current goal.
Assume Hu'a: SNo u'.
Assume _ _.
Apply SNoR_E y Hy v' Hv' to the current goal.
Assume Hv'a: SNo v'.
Assume _ _.
We prove the intermediate claim Lu'y: SNo (u' * y).
An exact proof term for the current goal is SNo_mul_SNo u' y Hu'a Hy.
We prove the intermediate claim Lxv': SNo (x * v').
An exact proof term for the current goal is SNo_mul_SNo x v' Hx Hv'a.
We prove the intermediate claim Lu'v': SNo (u' * v').
An exact proof term for the current goal is SNo_mul_SNo u' v' Hu'a Hv'a.
rewrite the current goal using Hwe (from left to right).
rewrite the current goal using Hze (from left to right).
We will prove u * y + x * v + - u * v < u' * y + x * v' + - u' * v'.
Apply add_SNo_minus_Lt_lem (u * y) (x * v) (u * v) (u' * y) (x * v') (u' * v') Luy Lxv Luv Lu'y Lxv' Lu'v' to the current goal.
We will prove u * y + x * v + u' * v' < u' * y + x * v' + u * v.
Apply SNoLt_tra (u * y + x * v + u' * v') (x * y + u * v + u' * v') (u' * y + x * v' + u * v) (SNo_add_SNo_3 (u * y) (x * v) (u' * v') Luy Lxv Lu'v') (SNo_add_SNo_3 (x * y) (u * v) (u' * v') Hxy Luv Lu'v') (SNo_add_SNo_3 (u' * y) (x * v') (u * v) Lu'y Lxv' Luv) to the current goal.
We will prove u * y + x * v + u' * v' < x * y + u * v + u' * v'.
Apply add_SNo_3_3_3_Lt1 (u * y) (x * v) (x * y) (u * v) (u' * v') Luy Lxv Hxy Luv Lu'v' to the current goal.
We will prove u * y + x * v < x * y + u * v.
An exact proof term for the current goal is Hxy2 u Hu v Hv.
We will prove x * y + u * v + u' * v' < u' * y + x * v' + u * v.
Apply add_SNo_3_2_3_Lt1 (x * y) (u' * v') (u' * y) (x * v') (u * v) Hxy Lu'v' Lu'y Lxv' Luv to the current goal.
We will prove u' * v' + x * y < u' * y + x * v'.
rewrite the current goal using add_SNo_com (u' * v') (x * y) Lu'v' Hxy (from left to right).
An exact proof term for the current goal is Hxy3 u' Hu' v' Hv'.
Let u' be given.
Assume Hu'.
Let v' be given.
Assume Hv' Hze.
Apply SNoR_E x Hx u' Hu' to the current goal.
Assume Hu'a: SNo u'.
Assume _ _.
Apply SNoL_E y Hy v' Hv' to the current goal.
Assume Hv'a: SNo v'.
Assume _ _.
We prove the intermediate claim Lu'y: SNo (u' * y).
An exact proof term for the current goal is SNo_mul_SNo u' y Hu'a Hy.
We prove the intermediate claim Lxv': SNo (x * v').
An exact proof term for the current goal is SNo_mul_SNo x v' Hx Hv'a.
We prove the intermediate claim Lu'v': SNo (u' * v').
An exact proof term for the current goal is SNo_mul_SNo u' v' Hu'a Hv'a.
rewrite the current goal using Hwe (from left to right).
rewrite the current goal using Hze (from left to right).
We will prove u * y + x * v + - u * v < u' * y + x * v' + - u' * v'.
Apply add_SNo_minus_Lt_lem (u * y) (x * v) (u * v) (u' * y) (x * v') (u' * v') Luy Lxv Luv Lu'y Lxv' Lu'v' to the current goal.
We will prove u * y + x * v + u' * v' < u' * y + x * v' + u * v.
Apply SNoLt_tra (u * y + x * v + u' * v') (x * y + u * v + u' * v') (u' * y + x * v' + u * v) (SNo_add_SNo_3 (u * y) (x * v) (u' * v') Luy Lxv Lu'v') (SNo_add_SNo_3 (x * y) (u * v) (u' * v') Hxy Luv Lu'v') (SNo_add_SNo_3 (u' * y) (x * v') (u * v) Lu'y Lxv' Luv) to the current goal.
We will prove u * y + x * v + u' * v' < x * y + u * v + u' * v'.
Apply add_SNo_3_3_3_Lt1 (u * y) (x * v) (x * y) (u * v) (u' * v') Luy Lxv Hxy Luv Lu'v' to the current goal.
We will prove u * y + x * v < x * y + u * v.
An exact proof term for the current goal is Hxy2 u Hu v Hv.
We will prove x * y + u * v + u' * v' < u' * y + x * v' + u * v.
Apply add_SNo_3_2_3_Lt1 (x * y) (u' * v') (u' * y) (x * v') (u * v) Hxy Lu'v' Lu'y Lxv' Luv to the current goal.
We will prove u' * v' + x * y < u' * y + x * v'.
rewrite the current goal using add_SNo_com (u' * v') (x * y) Lu'v' Hxy (from left to right).
An exact proof term for the current goal is Hxy4 u' Hu' v' Hv'.
An exact proof term for the current goal is Hp L R LLR HLE HLI1 HLI2 HRE HRI1 HRI2 He.
∎