Set P to be the term λx ⇒ ∀y, SNo y → ∀p : prop, (SNo (x * y) → (∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v) → (∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v) → p) → p of type set → prop.
We will prove ∀x, SNo x → P x.
Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IHx: ∀w ∈ SNoS_ (SNoLev x), P w.
Set Q to be the term λy ⇒ ∀p : prop, (SNo (x * y) → (∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v) → (∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v) → p) → p of type set → prop.
We will prove ∀y, SNo y → Q y.
Apply SNoLev_ind to the current goal.
Let y be given.
Assume Hy: SNo y.
Assume IHy: ∀z ∈ SNoS_ (SNoLev y), Q z.
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 Hxy.
We prove the intermediate claim LLx: ∀u ∈ SNoL x, ∀v, SNo v → SNo (u * v).
Let u be given.
Assume Hu.
Let v be given.
Assume Hv.
Apply IHx u (SNoL_SNoS x Hx u Hu) v Hv to the current goal.
Assume H1 _ _ _ _.
An exact proof term for the current goal is H1.
We prove the intermediate claim LRx: ∀u ∈ SNoR x, ∀v, SNo v → SNo (u * v).
Let u be given.
Assume Hu.
Let v be given.
Assume Hv.
Apply IHx u (SNoR_SNoS x Hx u Hu) v Hv to the current goal.
Assume H1 _ _ _ _.
An exact proof term for the current goal is H1.
We prove the intermediate claim LLxy: ∀u ∈ SNoL x, SNo (u * y).
Let u be given.
Assume Hu.
An exact proof term for the current goal is LLx u Hu y Hy.
We prove the intermediate claim LRxy: ∀u ∈ SNoR x, SNo (u * y).
Let u be given.
Assume Hu.
An exact proof term for the current goal is LRx u Hu y Hy.
We prove the intermediate claim LxLy: ∀v ∈ SNoL y, SNo (x * v).
Let v be given.
Assume Hv.
Apply IHy v (SNoL_SNoS y Hy v Hv) to the current goal.
Assume H1 _ _ _ _.
An exact proof term for the current goal is H1.
We prove the intermediate claim LxRy: ∀v ∈ SNoR y, SNo (x * v).
Let v be given.
Assume Hv.
Apply IHy v (SNoR_SNoS y Hy v Hv) to the current goal.
Assume H1 _ _ _ _.
An exact proof term for the current goal is H1.
We prove the intermediate claim LLR1: SNoCutP L R.
We will prove (∀x ∈ L, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ L, ∀y ∈ R, x < y).
Apply and3I to the current goal.
Let u be given.
Assume Hu.
Apply HLE u Hu to the current goal.
Let w0 be given.
Assume Hw0.
Let w1 be given.
Assume Hw1 Huw.
Apply SNoL_E y Hy w1 Hw1 to the current goal.
Assume Hw1a _ _.
We will prove SNo u.
rewrite the current goal using Huw (from left to right).
We will prove SNo (w0 * y + x * w1 + - w0 * w1).
Apply SNo_add_SNo to the current goal.
We will prove SNo (w0 * y).
An exact proof term for the current goal is LLxy w0 Hw0.
We will prove SNo (x * w1 + - w0 * w1).
Apply SNo_add_SNo to the current goal.
We will prove SNo (x * w1).
An exact proof term for the current goal is LxLy w1 Hw1.
We will prove SNo (- w0 * w1).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is LLx w0 Hw0 w1 Hw1a.
Let z0 be given.
Assume Hz0.
Let z1 be given.
Assume Hz1 Huz.
Apply SNoR_E y Hy z1 Hz1 to the current goal.
Assume Hz1a _ _.
We will prove SNo u.
rewrite the current goal using Huz (from left to right).
We will prove SNo (z0 * y + x * z1 + - z0 * z1).
Apply SNo_add_SNo to the current goal.
We will prove SNo (z0 * y).
An exact proof term for the current goal is LRxy z0 Hz0.
We will prove SNo (x * z1 + - z0 * z1).
Apply SNo_add_SNo to the current goal.
We will prove SNo (x * z1).
An exact proof term for the current goal is LxRy z1 Hz1.
We will prove SNo (- z0 * z1).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is LRx z0 Hz0 z1 Hz1a.
Let u be given.
Assume Hu.
Apply HRE u Hu to the current goal.
Let w0 be given.
Assume Hw0.
Let z1 be given.
Assume Hz1 Huw.
Apply SNoR_E y Hy z1 Hz1 to the current goal.
Assume Hz1a _ _.
We will prove SNo u.
rewrite the current goal using Huw (from left to right).
We will prove SNo (w0 * y + x * z1 + - w0 * z1).
Apply SNo_add_SNo to the current goal.
We will prove SNo (w0 * y).
An exact proof term for the current goal is LLxy w0 Hw0.
We will prove SNo (x * z1 + - w0 * z1).
Apply SNo_add_SNo to the current goal.
We will prove SNo (x * z1).
An exact proof term for the current goal is LxRy z1 Hz1.
We will prove SNo (- w0 * z1).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is LLx w0 Hw0 z1 Hz1a.
Let z0 be given.
Assume Hz0.
Let w1 be given.
Assume Hw1 Huz.
Apply SNoL_E y Hy w1 Hw1 to the current goal.
Assume Hw1a _ _.
We will prove SNo u.
rewrite the current goal using Huz (from left to right).
We will prove SNo (z0 * y + x * w1 + - z0 * w1).
Apply SNo_add_SNo to the current goal.
We will prove SNo (z0 * y).
An exact proof term for the current goal is LRxy z0 Hz0.
We will prove SNo (x * w1 + - z0 * w1).
Apply SNo_add_SNo to the current goal.
We will prove SNo (x * w1).
An exact proof term for the current goal is LxLy w1 Hw1.
We will prove SNo (- z0 * w1).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is LRx z0 Hz0 w1 Hw1a.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv.
We prove the intermediate claim Luvimp: ∀u0 v0 ∈ SNoS_ (SNoLev x), ∀u1 v1 ∈ SNoS_ (SNoLev y), ∀p : prop, (SNo (u0 * y) → SNo (x * u1) → SNo (u0 * u1) → SNo (v0 * y) → SNo (x * v1) → SNo (v0 * v1) → SNo (u0 * v1) → SNo (v0 * u1) → (u = u0 * y + x * u1 + - u0 * u1 → v = v0 * y + x * v1 + - v0 * v1 → u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1 → u < v) → p) → p.
Let u0 be given.
Assume Hu0.
Let v0 be given.
Assume Hv0.
Let u1 be given.
Assume Hu1.
Let v1 be given.
Assume Hv1.
Apply SNoS_E2 (SNoLev y) (SNoLev_ordinal y Hy) u1 Hu1 to the current goal.
Assume Hu1a: SNoLev u1 ∈ SNoLev y.
Assume Hu1b: ordinal (SNoLev u1).
Assume Hu1c: SNo u1.
Assume _.
Apply SNoS_E2 (SNoLev y) (SNoLev_ordinal y Hy) v1 Hv1 to the current goal.
Assume Hv1a: SNoLev v1 ∈ SNoLev y.
Assume Hv1b: ordinal (SNoLev v1).
Assume Hv1c: SNo v1.
Assume _.
We prove the intermediate claim Lu0u1: SNo (u0 * u1).
Apply IHx u0 Hu0 u1 Hu1c to the current goal.
Assume IHx0 _ _ _ _.
An exact proof term for the current goal is IHx0.
We prove the intermediate claim Lv0v1: SNo (v0 * v1).
Apply IHx v0 Hv0 v1 Hv1c to the current goal.
Assume IHx0 _ _ _ _.
An exact proof term for the current goal is IHx0.
We prove the intermediate claim Lu0y: SNo (u0 * y).
Apply IHx u0 Hu0 y Hy to the current goal.
Assume H _ _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lxu1: SNo (x * u1).
Apply IHy u1 Hu1 to the current goal.
Assume H _ _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lv0y: SNo (v0 * y).
Apply IHx v0 Hv0 y Hy to the current goal.
Assume H _ _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lxv1: SNo (x * v1).
Apply IHy v1 Hv1 to the current goal.
Assume H _ _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lu0v1: SNo (u0 * v1).
Apply IHx u0 Hu0 v1 Hv1c to the current goal.
Assume IHx0 _ _ _ _.
An exact proof term for the current goal is IHx0.
We prove the intermediate claim Lv0u1: SNo (v0 * u1).
Apply IHx v0 Hv0 u1 Hu1c to the current goal.
Assume IHx0 _ _ _ _.
An exact proof term for the current goal is IHx0.
Let p be given.
Assume Hp.
Apply Hp Lu0y Lxu1 Lu0u1 Lv0y Lxv1 Lv0v1 Lu0v1 Lv0u1 to the current goal.
Assume Hue Hve H1.
We will prove u < v.
rewrite the current goal using Hue (from left to right).
rewrite the current goal using Hve (from left to right).
Apply add_SNo_Lt1_cancel (u0 * y + x * u1 + - u0 * u1) (u0 * u1 + v0 * v1) (v0 * y + x * v1 + - v0 * v1) (SNo_add_SNo (u0 * y) (x * u1 + - u0 * u1) Lu0y (SNo_add_SNo (x * u1) (- u0 * u1) Lxu1 (SNo_minus_SNo (u0 * u1) Lu0u1))) (SNo_add_SNo (u0 * u1) (v0 * v1) Lu0u1 Lv0v1) (SNo_add_SNo (v0 * y) (x * v1 + - v0 * v1) Lv0y (SNo_add_SNo (x * v1) (- v0 * v1) Lxv1 (SNo_minus_SNo (v0 * v1) Lv0v1))) to the current goal.
We prove the intermediate claim L1: (u0 * y + x * u1 + - u0 * u1) + (u0 * u1 + v0 * v1) = u0 * y + x * u1 + v0 * v1.
An exact proof term for the current goal is add_SNo_minus_SNo_prop5 (u0 * y) (x * u1) (u0 * u1) (v0 * v1) Lu0y Lxu1 Lu0u1 Lv0v1.
We prove the intermediate claim L2: (v0 * y + x * v1 + - v0 * v1) + (u0 * u1 + v0 * v1) = v0 * y + x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com (u0 * u1) (v0 * v1) Lu0u1 Lv0v1 (from left to right).
An exact proof term for the current goal is add_SNo_minus_SNo_prop5 (v0 * y) (x * v1) (v0 * v1) (u0 * u1) Lv0y Lxv1 Lv0v1 Lu0u1.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using L2 (from left to right).
An exact proof term for the current goal is H1.
Apply HLE u Hu to the current goal.
Let u0 be given.
Assume Hu0.
Let u1 be given.
Assume Hu1 Hue.
Apply SNoL_E x Hx u0 Hu0 to the current goal.
Assume Hu0a: SNo u0.
Assume Hu0b: SNoLev u0 ∈ SNoLev x.
Assume Hu0c: u0 < x.
Apply SNoL_E y Hy u1 Hu1 to the current goal.
Assume Hu1a: SNo u1.
Assume Hu1b: SNoLev u1 ∈ SNoLev y.
Assume Hu1c: u1 < y.
Apply HRE v Hv to the current goal.
Let v0 be given.
Assume Hv0.
Let v1 be given.
Assume Hv1 Hve.
Apply SNoL_E x Hx v0 Hv0 to the current goal.
Assume Hv0a: SNo v0.
Assume Hv0b: SNoLev v0 ∈ SNoLev x.
Assume Hv0c: v0 < x.
Apply SNoR_E y Hy v1 Hv1 to the current goal.
Assume Hv1a: SNo v1.
Assume Hv1b: SNoLev v1 ∈ SNoLev y.
Assume Hv1c: y < v1.
Apply Luvimp u0 (SNoL_SNoS x Hx u0 Hu0) v0 (SNoL_SNoS x Hx v0 Hv0) u1 (SNoL_SNoS y Hy u1 Hu1) v1 (SNoR_SNoS y Hy v1 Hv1) to the current goal.
Assume Lu0y Lxu1 Lu0u1 Lv0y Lxv1 Lv0v1 Lu0v1 Lv0u1 Luv.
Apply Luv Hue Hve to the current goal.
We will prove u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
We prove the intermediate claim Lu1v1lt: u1 < v1.
An exact proof term for the current goal is SNoLt_tra u1 y v1 Hu1a Hy Hv1a Hu1c Hv1c.
We prove the intermediate claim L3: ∀z ∈ SNoL x, x * u1 + z * v1 < z * u1 + x * v1.
Let z be given.
Assume Hz.
We prove the intermediate claim Lzu1: SNo (z * u1).
An exact proof term for the current goal is LLx z Hz u1 Hu1a.
We prove the intermediate claim Lzv1: SNo (z * v1).
An exact proof term for the current goal is LLx z Hz v1 Hv1a.
Apply SNoLt_SNoL_or_SNoR_impred u1 v1 Hu1a Hv1a Lu1v1lt to the current goal.
Let w be given.
Assume Hwv1: w ∈ SNoL v1.
Assume Hwu1: w ∈ SNoR u1.
Apply SNoR_E u1 Hu1a w Hwu1 to the current goal.
Assume Hwu1a: SNo w.
Assume Hwu1b: SNoLev w ∈ SNoLev u1.
Assume Hwu1c: u1 < w.
We prove the intermediate claim LwSy: w ∈ SNoS_ (SNoLev y).
Apply SNoS_I2 w y Hwu1a Hy to the current goal.
We will prove SNoLev w ∈ SNoLev y.
An exact proof term for the current goal is ordinal_TransSet (SNoLev y) (SNoLev_ordinal y Hy) (SNoLev u1) Hu1b (SNoLev w) Hwu1b.
We prove the intermediate claim Lzw: SNo (z * w).
An exact proof term for the current goal is LLx z Hz w Hwu1a.
We prove the intermediate claim Lxw: SNo (x * w).
Apply IHy w LwSy to the current goal.
Assume H1 _ _ _ _.
An exact proof term for the current goal is H1.
We prove the intermediate claim L3a: z * v1 + x * w < x * v1 + z * w.
Apply IHy v1 (SNoR_SNoS y Hy v1 Hv1) to the current goal.
Assume _ IHy1 _ _ _.
An exact proof term for the current goal is IHy1 z Hz w Hwv1.
We prove the intermediate claim L3b: x * u1 + z * w < z * u1 + x * w.
Apply IHy u1 (SNoL_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ IHy3 _.
An exact proof term for the current goal is IHy3 z Hz w Hwu1.
An exact proof term for the current goal is add_SNo_Lt_subprop2 (x * u1) (z * v1) (z * u1) (x * v1) (z * w) (x * w) Lxu1 Lzv1 Lzu1 Lxv1 Lzw Lxw L3b L3a.
Assume Hu1v1: u1 ∈ SNoL v1.
Apply IHy v1 (SNoR_SNoS y Hy v1 Hv1) to the current goal.
Assume _ IHy1 _ _ _.
rewrite the current goal using add_SNo_com (x * u1) (z * v1) Lxu1 Lzv1 (from left to right).
rewrite the current goal using add_SNo_com (z * u1) (x * v1) Lzu1 Lxv1 (from left to right).
We will prove z * v1 + x * u1 < x * v1 + z * u1.
An exact proof term for the current goal is IHy1 z Hz u1 Hu1v1.
Assume Hv1u1: v1 ∈ SNoR u1.
Apply IHy u1 (SNoL_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ IHy3 _.
An exact proof term for the current goal is IHy3 z Hz v1 Hv1u1.
We prove the intermediate claim L3u0: x * u1 + u0 * v1 < u0 * u1 + x * v1.
An exact proof term for the current goal is L3 u0 Hu0.
We prove the intermediate claim L3v0: x * u1 + v0 * v1 < v0 * u1 + x * v1.
An exact proof term for the current goal is L3 v0 Hv0.
We prove the intermediate claim L3u0imp: u0 * y + v0 * v1 < v0 * y + u0 * v1 → u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
Assume H1.
Apply add_SNo_Lt_subprop3a (u0 * y) (x * u1) (v0 * v1) (v0 * y) (x * v1 + u0 * u1) (u0 * v1) Lu0y Lxu1 Lv0v1 Lv0y (SNo_add_SNo (x * v1) (u0 * u1) Lxv1 Lu0u1) Lu0v1 H1 to the current goal.
We will prove x * u1 + u0 * v1 < x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com (x * v1) (u0 * u1) Lxv1 Lu0u1 (from left to right).
An exact proof term for the current goal is L3u0.
We prove the intermediate claim L3v0imp: u0 * y + v0 * u1 < v0 * y + u0 * u1 → u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
Assume H1.
Apply add_SNo_Lt_subprop3b (u0 * y) (x * u1 + v0 * v1) (v0 * y) (x * v1) (u0 * u1) (v0 * u1) Lu0y (SNo_add_SNo (x * u1) (v0 * v1) Lxu1 Lv0v1) Lv0y Lxv1 Lu0u1 Lv0u1 to the current goal.
We will prove u0 * y + v0 * u1 < v0 * y + u0 * u1.
An exact proof term for the current goal is H1.
We will prove x * u1 + v0 * v1 < v0 * u1 + x * v1.
An exact proof term for the current goal is L3v0.
Apply SNoL_or_SNoR_impred v0 u0 Hv0a Hu0a to the current goal.
Assume Hv0u0: v0 = u0.
rewrite the current goal using Hv0u0 (from left to right).
We will prove u0 * y + (x * u1 + u0 * v1) < u0 * y + (x * v1 + u0 * u1).
Apply add_SNo_Lt2 (u0 * y) (x * u1 + u0 * v1) (x * v1 + u0 * u1) Lu0y (SNo_add_SNo (x * u1) (u0 * v1) Lxu1 Lu0v1) (SNo_add_SNo (x * v1) (u0 * u1) Lxv1 Lu0u1) to the current goal.
We will prove x * u1 + u0 * v1 < x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com (x * v1) (u0 * u1) Lxv1 Lu0u1 (from left to right).
An exact proof term for the current goal is L3u0.
Let z be given.
Assume Hzu0: z ∈ SNoL u0.
Assume Hzv0: z ∈ SNoR v0.
We prove the intermediate claim L4: u0 * y + z * v1 < z * y + u0 * v1.
Apply IHx u0 (SNoL_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ IHx3 _.
An exact proof term for the current goal is IHx3 z Hzu0 v1 Hv1.
We prove the intermediate claim L5: z * y + v0 * v1 < v0 * y + z * v1.
Apply IHx v0 (SNoL_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ _ IHx2 _ _.
An exact proof term for the current goal is IHx2 z Hzv0 v1 Hv1.
We prove the intermediate claim Lz: z ∈ SNoL x.
Apply SNoL_E u0 Hu0a z Hzu0 to the current goal.
Assume Hza: SNo z.
Assume Hzb: SNoLev z ∈ SNoLev u0.
Assume Hzc: z < u0.
Apply SNoL_I x Hx z Hza to the current goal.
We will prove SNoLev z ∈ SNoLev x.
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) (SNoLev u0) Hu0b (SNoLev z) Hzb.
We will prove z < x.
An exact proof term for the current goal is SNoLt_tra z u0 x Hza Hu0a Hx Hzc Hu0c.
Apply add_SNo_Lt_subprop3c (u0 * y) (x * u1) (v0 * v1) (v0 * y) (x * v1 + u0 * u1) (z * v1) (z * y) (u0 * v1) Lu0y Lxu1 Lv0v1 Lv0y (SNo_add_SNo (x * v1) (u0 * u1) Lxv1 Lu0u1) (LLx z Lz v1 Hv1a) (LLxy z Lz) Lu0v1 to the current goal.
An exact proof term for the current goal is L4.
rewrite the current goal using add_SNo_com (x * v1) (u0 * u1) Lxv1 Lu0u1 (from left to right).
An exact proof term for the current goal is L3u0.
An exact proof term for the current goal is L5.
Assume Hv0u0: v0 ∈ SNoL u0.
Apply L3u0imp to the current goal.
We will prove u0 * y + v0 * v1 < v0 * y + u0 * v1.
Apply IHx u0 (SNoL_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ IHx3 _.
An exact proof term for the current goal is IHx3 v0 Hv0u0 v1 Hv1.
Assume Hu0v0: u0 ∈ SNoR v0.
Apply L3u0imp to the current goal.
We will prove u0 * y + v0 * v1 < v0 * y + u0 * v1.
Apply IHx v0 (SNoL_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ _ IHx2 _ _.
An exact proof term for the current goal is IHx2 u0 Hu0v0 v1 Hv1.
Let z be given.
Assume Hzu0: z ∈ SNoR u0.
Assume Hzv0: z ∈ SNoL v0.
We prove the intermediate claim L6: z * y + v0 * u1 < v0 * y + z * u1.
Apply IHx v0 (SNoL_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ IHx1 _ _ _.
An exact proof term for the current goal is IHx1 z Hzv0 u1 Hu1.
We prove the intermediate claim L7: u0 * y + z * u1 < z * y + u0 * u1.
Apply IHx u0 (SNoL_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ _ IHx4.
An exact proof term for the current goal is IHx4 z Hzu0 u1 Hu1.
We prove the intermediate claim Lz: z ∈ SNoL x.
Apply SNoL_E v0 Hv0a z Hzv0 to the current goal.
Assume Hza: SNo z.
Assume Hzb: SNoLev z ∈ SNoLev v0.
Assume Hzc: z < v0.
Apply SNoL_I x Hx z Hza to the current goal.
We will prove SNoLev z ∈ SNoLev x.
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) (SNoLev v0) Hv0b (SNoLev z) Hzb.
We will prove z < x.
An exact proof term for the current goal is SNoLt_tra z v0 x Hza Hv0a Hx Hzc Hv0c.
An exact proof term for the current goal is add_SNo_Lt_subprop3d (u0 * y) (x * u1 + v0 * v1) (v0 * y) (x * v1) (u0 * u1) (z * u1) (z * y) (v0 * u1) Lu0y (SNo_add_SNo (x * u1) (v0 * v1) Lxu1 Lv0v1) Lv0y Lxv1 Lu0u1 (LLx z Lz u1 Hu1a) (LLxy z Lz) Lv0u1 L7 L3v0 L6.
Assume Hv0u0: v0 ∈ SNoR u0.
Apply L3v0imp to the current goal.
We will prove u0 * y + v0 * u1 < v0 * y + u0 * u1.
Apply IHx u0 (SNoL_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ _ IHx4.
An exact proof term for the current goal is IHx4 v0 Hv0u0 u1 Hu1.
Assume Hu0v0: u0 ∈ SNoL v0.
Apply L3v0imp to the current goal.
We will prove u0 * y + v0 * u1 < v0 * y + u0 * u1.
Apply IHx v0 (SNoL_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ IHx1 _ _ _.
An exact proof term for the current goal is IHx1 u0 Hu0v0 u1 Hu1.
Let v0 be given.
Assume Hv0.
Let v1 be given.
Assume Hv1 Hve.
Apply SNoR_E x Hx v0 Hv0 to the current goal.
Assume Hv0a: SNo v0.
Assume Hv0b: SNoLev v0 ∈ SNoLev x.
Assume Hv0c: x < v0.
Apply SNoL_E y Hy v1 Hv1 to the current goal.
Assume Hv1a: SNo v1.
Assume Hv1b: SNoLev v1 ∈ SNoLev y.
Assume Hv1c: v1 < y.
Apply Luvimp u0 (SNoL_SNoS x Hx u0 Hu0) v0 (SNoR_SNoS x Hx v0 Hv0) u1 (SNoL_SNoS y Hy u1 Hu1) v1 (SNoL_SNoS y Hy v1 Hv1) to the current goal.
Assume Lu0y Lxu1 Lu0u1 Lv0y Lxv1 Lv0v1 Lu0v1 Lv0u1 Luv.
Apply Luv Hue Hve to the current goal.
We will prove u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
We prove the intermediate claim Lu0v0lt: u0 < v0.
An exact proof term for the current goal is SNoLt_tra u0 x v0 Hu0a Hx Hv0a Hu0c Hv0c.
We prove the intermediate claim L3: ∀z ∈ SNoL y, u0 * y + v0 * z < v0 * y + u0 * z.
Let z be given.
Assume Hz.
Apply SNoL_E y Hy z Hz to the current goal.
Assume Hza: SNo z.
Assume Hzb: SNoLev z ∈ SNoLev y.
Assume Hzc: z < y.
We prove the intermediate claim Lu0z: SNo (u0 * z).
An exact proof term for the current goal is LLx u0 Hu0 z Hza.
We prove the intermediate claim Lv0z: SNo (v0 * z).
An exact proof term for the current goal is LRx v0 Hv0 z Hza.
Apply SNoLt_SNoL_or_SNoR_impred u0 v0 Hu0a Hv0a Lu0v0lt to the current goal.
Let w be given.
Assume Hwv0: w ∈ SNoL v0.
Assume Hwu0: w ∈ SNoR u0.
Apply SNoR_E u0 Hu0a w Hwu0 to the current goal.
Assume Hwu0a: SNo w.
Assume Hwu0b: SNoLev w ∈ SNoLev u0.
Assume Hwu0c: u0 < w.
We prove the intermediate claim LLevwLevx: SNoLev w ∈ SNoLev x.
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) (SNoLev u0) Hu0b (SNoLev w) Hwu0b.
We prove the intermediate claim LwSx: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hwu0a Hx LLevwLevx.
We prove the intermediate claim Lwz: SNo (w * z).
Apply IHx w LwSx z Hza to the current goal.
Assume H _ _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lwy: SNo (w * y).
Apply IHx w LwSx y Hy to the current goal.
Assume H _ _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim L3a: u0 * y + w * z < u0 * z + w * y.
rewrite the current goal using add_SNo_com (u0 * z) (w * y) Lu0z Lwy (from left to right).
Apply IHx u0 (SNoL_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ _ IHx4.
An exact proof term for the current goal is IHx4 w Hwu0 z Hz.
We prove the intermediate claim L3b: v0 * z + w * y < v0 * y + w * z.
rewrite the current goal using add_SNo_com (v0 * z) (w * y) Lv0z Lwy (from left to right).
Apply IHx v0 (SNoR_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ IHx1 _ _ _.
An exact proof term for the current goal is IHx1 w Hwv0 z Hz.
rewrite the current goal using add_SNo_com (u0 * z) (v0 * y) Lu0z Lv0y (from right to left).
An exact proof term for the current goal is add_SNo_Lt_subprop2 (u0 * y) (v0 * z) (u0 * z) (v0 * y) (w * z) (w * y) Lu0y Lv0z Lu0z Lv0y Lwz Lwy L3a L3b.
Assume Hu0v0: u0 ∈ SNoL v0.
Apply IHx v0 (SNoR_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ IHx1 _ _ _.
An exact proof term for the current goal is IHx1 u0 Hu0v0 z Hz.
Assume Hv0u0: v0 ∈ SNoR u0.
Apply IHx u0 (SNoL_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ _ IHx4.
An exact proof term for the current goal is IHx4 v0 Hv0u0 z Hz.
We prove the intermediate claim L3u1: u0 * y + v0 * u1 < v0 * y + u0 * u1.
An exact proof term for the current goal is L3 u1 Hu1.
We prove the intermediate claim L3v1: u0 * y + v0 * v1 < v0 * y + u0 * v1.
An exact proof term for the current goal is L3 v1 Hv1.
We prove the intermediate claim L3u1imp: x * u1 + v0 * v1 < v0 * u1 + x * v1 → u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
An exact proof term for the current goal is add_SNo_Lt_subprop3b (u0 * y) (x * u1 + v0 * v1) (v0 * y) (x * v1) (u0 * u1) (v0 * u1) Lu0y (SNo_add_SNo (x * u1) (v0 * v1) Lxu1 Lv0v1) Lv0y Lxv1 Lu0u1 Lv0u1 L3u1.
We prove the intermediate claim L3v1imp: x * u1 + u0 * v1 < x * v1 + u0 * u1 → u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
An exact proof term for the current goal is add_SNo_Lt_subprop3a (u0 * y) (x * u1) (v0 * v1) (v0 * y) (x * v1 + u0 * u1) (u0 * v1) Lu0y Lxu1 Lv0v1 Lv0y (SNo_add_SNo (x * v1) (u0 * u1) Lxv1 Lu0u1) Lu0v1 L3v1.
Apply SNoL_or_SNoR_impred v1 u1 Hv1a Hu1a to the current goal.
Assume Hv1u1: v1 = u1.
rewrite the current goal using Hv1u1 (from left to right).
We will prove u0 * y + x * u1 + v0 * u1 < v0 * y + x * u1 + u0 * u1.
rewrite the current goal using add_SNo_com_3_0_1 (u0 * y) (x * u1) (v0 * u1) Lu0y Lxu1 Lv0u1 (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (v0 * y) (x * u1) (u0 * u1) Lv0y Lxu1 Lu0u1 (from left to right).
Apply add_SNo_Lt2 (x * u1) (u0 * y + v0 * u1) (v0 * y + u0 * u1) Lxu1 (SNo_add_SNo (u0 * y) (v0 * u1) Lu0y Lv0u1) (SNo_add_SNo (v0 * y) (u0 * u1) Lv0y Lu0u1) to the current goal.
We will prove u0 * y + v0 * u1 < v0 * y + u0 * u1.
An exact proof term for the current goal is L3u1.
Let z be given.
Assume Hzu1: z ∈ SNoL u1.
Assume Hzv1: z ∈ SNoR v1.
Apply SNoL_E u1 Hu1a z Hzu1 to the current goal.
Assume Hza: SNo z.
Assume Hzb: SNoLev z ∈ SNoLev u1.
Assume Hzc: z < u1.
We prove the intermediate claim Lz: z ∈ SNoL y.
Apply SNoL_I y Hy z Hza to the current goal.
We will prove SNoLev z ∈ SNoLev y.
An exact proof term for the current goal is ordinal_TransSet (SNoLev y) (SNoLev_ordinal y Hy) (SNoLev u1) Hu1b (SNoLev z) Hzb.
We will prove z < y.
An exact proof term for the current goal is SNoLt_tra z u1 y Hza Hu1a Hy Hzc Hu1c.
We prove the intermediate claim L4: x * u1 + v0 * z < x * z + v0 * u1.
rewrite the current goal using add_SNo_com (x * z) (v0 * u1) (LxLy z Lz) Lv0u1 (from left to right).
We will prove x * u1 + v0 * z < v0 * u1 + x * z.
Apply IHy u1 (SNoL_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ _ IHy4.
An exact proof term for the current goal is IHy4 v0 Hv0 z Hzu1.
We prove the intermediate claim L5: x * z + v0 * v1 < x * v1 + v0 * z.
rewrite the current goal using add_SNo_com (x * z) (v0 * v1) (LxLy z Lz) Lv0v1 (from left to right).
Apply IHy v1 (SNoL_SNoS y Hy v1 Hv1) to the current goal.
Assume _ _ IHy2 _ _.
An exact proof term for the current goal is IHy2 v0 Hv0 z Hzv1.
We will prove u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com_3_0_1 (u0 * y) (x * u1) (v0 * v1) Lu0y Lxu1 Lv0v1 (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (v0 * y) (x * v1) (u0 * u1) Lv0y Lxv1 Lu0u1 (from left to right).
We will prove x * u1 + u0 * y + v0 * v1 < x * v1 + v0 * y + u0 * u1.
An exact proof term for the current goal is add_SNo_Lt_subprop3c (x * u1) (u0 * y) (v0 * v1) (x * v1) (v0 * y + u0 * u1) (v0 * z) (x * z) (v0 * u1) Lxu1 Lu0y Lv0v1 Lxv1 (SNo_add_SNo (v0 * y) (u0 * u1) Lv0y Lu0u1) (LRx v0 Hv0 z Hza) (LxLy z Lz) Lv0u1 L4 L3u1 L5.
Assume Hv1u1: v1 ∈ SNoL u1.
Apply L3u1imp to the current goal.
We will prove x * u1 + v0 * v1 < v0 * u1 + x * v1.
Apply IHy u1 (SNoL_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ _ IHy4.
An exact proof term for the current goal is IHy4 v0 Hv0 v1 Hv1u1.
Assume Hu1v1: u1 ∈ SNoR v1.
Apply L3u1imp to the current goal.
We will prove x * u1 + v0 * v1 < v0 * u1 + x * v1.
rewrite the current goal using add_SNo_com (x * u1) (v0 * v1) Lxu1 Lv0v1 (from left to right).
rewrite the current goal using add_SNo_com (v0 * u1) (x * v1) Lv0u1 Lxv1 (from left to right).
Apply IHy v1 (SNoL_SNoS y Hy v1 Hv1) to the current goal.
Assume _ _ IHy2 _ _.
An exact proof term for the current goal is IHy2 v0 Hv0 u1 Hu1v1.
Let z be given.
Assume Hzu1: z ∈ SNoR u1.
Assume Hzv1: z ∈ SNoL v1.
Apply SNoL_E v1 Hv1a z Hzv1 to the current goal.
Assume Hza: SNo z.
Assume Hzb: SNoLev z ∈ SNoLev v1.
Assume Hzc: z < v1.
We prove the intermediate claim Lz: z ∈ SNoL y.
Apply SNoL_I y Hy z Hza to the current goal.
We will prove SNoLev z ∈ SNoLev y.
An exact proof term for the current goal is ordinal_TransSet (SNoLev y) (SNoLev_ordinal y Hy) (SNoLev v1) Hv1b (SNoLev z) Hzb.
We will prove z < y.
An exact proof term for the current goal is SNoLt_tra z v1 y Hza Hv1a Hy Hzc Hv1c.
We prove the intermediate claim L6: x * u1 + u0 * z < x * z + u0 * u1.
rewrite the current goal using add_SNo_com (x * z) (u0 * u1) (LxLy z Lz) Lu0u1 (from left to right).
Apply IHy u1 (SNoL_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ IHy3 _.
An exact proof term for the current goal is IHy3 u0 Hu0 z Hzu1.
We prove the intermediate claim L7: x * z + u0 * v1 < x * v1 + u0 * z.
rewrite the current goal using add_SNo_com (x * z) (u0 * v1) (LxLy z Lz) Lu0v1 (from left to right).
Apply IHy v1 (SNoL_SNoS y Hy v1 Hv1) to the current goal.
Assume _ IHy1 _ _ _.
An exact proof term for the current goal is IHy1 u0 Hu0 z Hzv1.
We will prove u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com_3_0_1 (u0 * y) (x * u1) (v0 * v1) Lu0y Lxu1 Lv0v1 (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (v0 * y) (x * v1) (u0 * u1) Lv0y Lxv1 Lu0u1 (from left to right).
We will prove x * u1 + u0 * y + v0 * v1 < x * v1 + v0 * y + u0 * u1.
Apply add_SNo_Lt_subprop3d (x * u1) (u0 * y + v0 * v1) (x * v1) (v0 * y) (u0 * u1) (u0 * z) (x * z) (u0 * v1) Lxu1 (SNo_add_SNo (u0 * y) (v0 * v1) Lu0y Lv0v1) Lxv1 Lv0y Lu0u1 (LLx u0 Hu0 z Hza) (LxLy z Lz) Lu0v1 L6 to the current goal.
We will prove u0 * y + v0 * v1 < u0 * v1 + v0 * y.
rewrite the current goal using add_SNo_com (u0 * v1) (v0 * y) Lu0v1 Lv0y (from left to right).
An exact proof term for the current goal is L3v1.
An exact proof term for the current goal is L7.
Assume Hv1u1: v1 ∈ SNoR u1.
Apply L3v1imp to the current goal.
We will prove x * u1 + u0 * v1 < x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com (x * v1) (u0 * u1) Lxv1 Lu0u1 (from left to right).
Apply IHy u1 (SNoL_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ IHy3 _.
An exact proof term for the current goal is IHy3 u0 Hu0 v1 Hv1u1.
Assume Hu1v1: u1 ∈ SNoL v1.
Apply L3v1imp to the current goal.
We will prove x * u1 + u0 * v1 < x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com (x * u1) (u0 * v1) Lxu1 Lu0v1 (from left to right).
Apply IHy v1 (SNoL_SNoS y Hy v1 Hv1) to the current goal.
Assume _ IHy1 _ _ _.
An exact proof term for the current goal is IHy1 u0 Hu0 u1 Hu1v1.
Let u0 be given.
Assume Hu0.
Let u1 be given.
Assume Hu1 Hue.
Apply SNoR_E x Hx u0 Hu0 to the current goal.
Assume Hu0a: SNo u0.
Assume Hu0b: SNoLev u0 ∈ SNoLev x.
Assume Hu0c: x < u0.
Apply SNoR_E y Hy u1 Hu1 to the current goal.
Assume Hu1a: SNo u1.
Assume Hu1b: SNoLev u1 ∈ SNoLev y.
Assume Hu1c: y < u1.
Apply HRE v Hv to the current goal.
Let v0 be given.
Assume Hv0.
Let v1 be given.
Assume Hv1 Hve.
Apply SNoL_E x Hx v0 Hv0 to the current goal.
Assume Hv0a: SNo v0.
Assume Hv0b: SNoLev v0 ∈ SNoLev x.
Assume Hv0c: v0 < x.
Apply SNoR_E y Hy v1 Hv1 to the current goal.
Assume Hv1a: SNo v1.
Assume Hv1b: SNoLev v1 ∈ SNoLev y.
Assume Hv1c: y < v1.
Apply Luvimp u0 (SNoR_SNoS x Hx u0 Hu0) v0 (SNoL_SNoS x Hx v0 Hv0) u1 (SNoR_SNoS y Hy u1 Hu1) v1 (SNoR_SNoS y Hy v1 Hv1) to the current goal.
Assume Lu0y Lxu1 Lu0u1 Lv0y Lxv1 Lv0v1 Lu0v1 Lv0u1 Luv.
Apply Luv Hue Hve to the current goal.
We will prove u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
We prove the intermediate claim Lv0u0lt: v0 < u0.
An exact proof term for the current goal is SNoLt_tra v0 x u0 Hv0a Hx Hu0a Hv0c Hu0c.
We prove the intermediate claim L3: ∀z ∈ SNoR y, u0 * y + v0 * z < v0 * y + u0 * z.
Let z be given.
Assume Hz.
Apply SNoR_E y Hy z Hz to the current goal.
Assume Hza: SNo z.
Assume Hzb: SNoLev z ∈ SNoLev y.
Assume Hzc: y < z.
We prove the intermediate claim Lu0z: SNo (u0 * z).
An exact proof term for the current goal is LRx u0 Hu0 z Hza.
We prove the intermediate claim Lv0z: SNo (v0 * z).
An exact proof term for the current goal is LLx v0 Hv0 z Hza.
Apply SNoLt_SNoL_or_SNoR_impred v0 u0 Hv0a Hu0a Lv0u0lt to the current goal.
Let w be given.
Assume Hwu0: w ∈ SNoL u0.
Assume Hwv0: w ∈ SNoR v0.
Apply SNoL_E u0 Hu0a w Hwu0 to the current goal.
Assume Hwu0a: SNo w.
Assume Hwu0b: SNoLev w ∈ SNoLev u0.
Assume Hwu0c: w < u0.
We prove the intermediate claim LLevwLevx: SNoLev w ∈ SNoLev x.
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) (SNoLev u0) Hu0b (SNoLev w) Hwu0b.
We prove the intermediate claim LwSx: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hwu0a Hx LLevwLevx.
We prove the intermediate claim Lwz: SNo (w * z).
Apply IHx w LwSx z Hza to the current goal.
Assume H _ _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lwy: SNo (w * y).
Apply IHx w LwSx y Hy to the current goal.
Assume H _ _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim L3a: u0 * y + w * z < u0 * z + w * y.
rewrite the current goal using add_SNo_com (u0 * z) (w * y) Lu0z Lwy (from left to right).
Apply IHx u0 (SNoR_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ IHx3 _.
An exact proof term for the current goal is IHx3 w Hwu0 z Hz.
We prove the intermediate claim L3b: v0 * z + w * y < v0 * y + w * z.
rewrite the current goal using add_SNo_com (v0 * z) (w * y) Lv0z Lwy (from left to right).
Apply IHx v0 (SNoL_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ _ IHx2 _ _.
An exact proof term for the current goal is IHx2 w Hwv0 z Hz.
rewrite the current goal using add_SNo_com (v0 * y) (u0 * z) Lv0y Lu0z (from left to right).
An exact proof term for the current goal is add_SNo_Lt_subprop2 (u0 * y) (v0 * z) (u0 * z) (v0 * y) (w * z) (w * y) Lu0y Lv0z Lu0z Lv0y Lwz Lwy L3a L3b.
Assume Hv0u0: v0 ∈ SNoL u0.
Apply IHx u0 (SNoR_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ IHx3 _.
An exact proof term for the current goal is IHx3 v0 Hv0u0 z Hz.
Assume Hu0v0: u0 ∈ SNoR v0.
Apply IHx v0 (SNoL_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ _ IHx2 _ _.
An exact proof term for the current goal is IHx2 u0 Hu0v0 z Hz.
We prove the intermediate claim L3u1: u0 * y + v0 * u1 < v0 * y + u0 * u1.
An exact proof term for the current goal is L3 u1 Hu1.
We prove the intermediate claim L3v1: u0 * y + v0 * v1 < v0 * y + u0 * v1.
An exact proof term for the current goal is L3 v1 Hv1.
We prove the intermediate claim L3u1imp: x * u1 + v0 * v1 < v0 * u1 + x * v1 → u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
An exact proof term for the current goal is add_SNo_Lt_subprop3b (u0 * y) (x * u1 + v0 * v1) (v0 * y) (x * v1) (u0 * u1) (v0 * u1) Lu0y (SNo_add_SNo (x * u1) (v0 * v1) Lxu1 Lv0v1) Lv0y Lxv1 Lu0u1 Lv0u1 L3u1.
We prove the intermediate claim L3v1imp: x * u1 + u0 * v1 < x * v1 + u0 * u1 → u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
An exact proof term for the current goal is add_SNo_Lt_subprop3a (u0 * y) (x * u1) (v0 * v1) (v0 * y) (x * v1 + u0 * u1) (u0 * v1) Lu0y Lxu1 Lv0v1 Lv0y (SNo_add_SNo (x * v1) (u0 * u1) Lxv1 Lu0u1) Lu0v1 L3v1.
Apply SNoL_or_SNoR_impred v1 u1 Hv1a Hu1a to the current goal.
Assume Hv1u1: v1 = u1.
rewrite the current goal using Hv1u1 (from left to right).
We will prove u0 * y + x * u1 + v0 * u1 < v0 * y + x * u1 + u0 * u1.
rewrite the current goal using add_SNo_com_3_0_1 (u0 * y) (x * u1) (v0 * u1) Lu0y Lxu1 Lv0u1 (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (v0 * y) (x * u1) (u0 * u1) Lv0y Lxu1 Lu0u1 (from left to right).
Apply add_SNo_Lt2 (x * u1) (u0 * y + v0 * u1) (v0 * y + u0 * u1) Lxu1 (SNo_add_SNo (u0 * y) (v0 * u1) Lu0y Lv0u1) (SNo_add_SNo (v0 * y) (u0 * u1) Lv0y Lu0u1) to the current goal.
We will prove u0 * y + v0 * u1 < v0 * y + u0 * u1.
An exact proof term for the current goal is L3u1.
Let z be given.
Assume Hzu1: z ∈ SNoL u1.
Assume Hzv1: z ∈ SNoR v1.
Apply SNoR_E v1 Hv1a z Hzv1 to the current goal.
Assume Hza: SNo z.
Assume Hzb: SNoLev z ∈ SNoLev v1.
Assume Hzc: v1 < z.
We prove the intermediate claim Lz: z ∈ SNoR y.
Apply SNoR_I y Hy z Hza to the current goal.
We will prove SNoLev z ∈ SNoLev y.
An exact proof term for the current goal is ordinal_TransSet (SNoLev y) (SNoLev_ordinal y Hy) (SNoLev v1) Hv1b (SNoLev z) Hzb.
We will prove y < z.
An exact proof term for the current goal is SNoLt_tra y v1 z Hy Hv1a Hza Hv1c Hzc.
We prove the intermediate claim L4: x * u1 + u0 * z < x * z + u0 * u1.
rewrite the current goal using add_SNo_com (x * z) (u0 * u1) (LxRy z Lz) Lu0u1 (from left to right).
Apply IHy u1 (SNoR_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ _ IHy4.
An exact proof term for the current goal is IHy4 u0 Hu0 z Hzu1.
We prove the intermediate claim L5: x * z + u0 * v1 < x * v1 + u0 * z.
rewrite the current goal using add_SNo_com (x * z) (u0 * v1) (LxRy z Lz) Lu0v1 (from left to right).
Apply IHy v1 (SNoR_SNoS y Hy v1 Hv1) to the current goal.
Assume _ _ IHy2 _ _.
An exact proof term for the current goal is IHy2 u0 Hu0 z Hzv1.
We will prove u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com_3_0_1 (u0 * y) (x * u1) (v0 * v1) Lu0y Lxu1 Lv0v1 (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (v0 * y) (x * v1) (u0 * u1) Lv0y Lxv1 Lu0u1 (from left to right).
We will prove x * u1 + u0 * y + v0 * v1 < x * v1 + v0 * y + u0 * u1.
Apply add_SNo_Lt_subprop3d (x * u1) (u0 * y + v0 * v1) (x * v1) (v0 * y) (u0 * u1) (u0 * z) (x * z) (u0 * v1) Lxu1 (SNo_add_SNo (u0 * y) (v0 * v1) Lu0y Lv0v1) Lxv1 Lv0y Lu0u1 (LRx u0 Hu0 z Hza) (LxRy z Lz) Lu0v1 L4 to the current goal.
We will prove u0 * y + v0 * v1 < u0 * v1 + v0 * y.
rewrite the current goal using add_SNo_com (u0 * v1) (v0 * y) Lu0v1 Lv0y (from left to right).
An exact proof term for the current goal is L3v1.
An exact proof term for the current goal is L5.
Assume Hv1u1: v1 ∈ SNoL u1.
Apply L3v1imp to the current goal.
We will prove x * u1 + u0 * v1 < x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com (x * v1) (u0 * u1) Lxv1 Lu0u1 (from left to right).
We will prove x * u1 + u0 * v1 < u0 * u1 + x * v1.
Apply IHy u1 (SNoR_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ _ IHy4.
An exact proof term for the current goal is IHy4 u0 Hu0 v1 Hv1u1.
Assume Hu1v1: u1 ∈ SNoR v1.
Apply L3v1imp to the current goal.
We will prove x * u1 + u0 * v1 < x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com (x * u1) (u0 * v1) Lxu1 Lu0v1 (from left to right).
Apply IHy v1 (SNoR_SNoS y Hy v1 Hv1) to the current goal.
Assume _ _ IHy2 _ _.
An exact proof term for the current goal is IHy2 u0 Hu0 u1 Hu1v1.
Let z be given.
Assume Hzu1: z ∈ SNoR u1.
Assume Hzv1: z ∈ SNoL v1.
Apply SNoR_E u1 Hu1a z Hzu1 to the current goal.
Assume Hza: SNo z.
Assume Hzb: SNoLev z ∈ SNoLev u1.
Assume Hzc: u1 < z.
We prove the intermediate claim Lz: z ∈ SNoR y.
Apply SNoR_I y Hy z Hza to the current goal.
We will prove SNoLev z ∈ SNoLev y.
An exact proof term for the current goal is ordinal_TransSet (SNoLev y) (SNoLev_ordinal y Hy) (SNoLev u1) Hu1b (SNoLev z) Hzb.
We will prove y < z.
An exact proof term for the current goal is SNoLt_tra y u1 z Hy Hu1a Hza Hu1c Hzc.
We prove the intermediate claim L6: x * u1 + v0 * z < x * z + v0 * u1.
rewrite the current goal using add_SNo_com (x * z) (v0 * u1) (LxRy z Lz) Lv0u1 (from left to right).
We will prove x * u1 + v0 * z < v0 * u1 + x * z.
Apply IHy u1 (SNoR_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ IHy3 _.
An exact proof term for the current goal is IHy3 v0 Hv0 z Hzu1.
We prove the intermediate claim L7: x * z + v0 * v1 < x * v1 + v0 * z.
rewrite the current goal using add_SNo_com (x * z) (v0 * v1) (LxRy z Lz) Lv0v1 (from left to right).
Apply IHy v1 (SNoR_SNoS y Hy v1 Hv1) to the current goal.
Assume _ IHy1 _ _ _.
An exact proof term for the current goal is IHy1 v0 Hv0 z Hzv1.
We will prove u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com_3_0_1 (u0 * y) (x * u1) (v0 * v1) Lu0y Lxu1 Lv0v1 (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (v0 * y) (x * v1) (u0 * u1) Lv0y Lxv1 Lu0u1 (from left to right).
We will prove x * u1 + u0 * y + v0 * v1 < x * v1 + v0 * y + u0 * u1.
An exact proof term for the current goal is add_SNo_Lt_subprop3c (x * u1) (u0 * y) (v0 * v1) (x * v1) (v0 * y + u0 * u1) (v0 * z) (x * z) (v0 * u1) Lxu1 Lu0y Lv0v1 Lxv1 (SNo_add_SNo (v0 * y) (u0 * u1) Lv0y Lu0u1) (LLx v0 Hv0 z Hza) (LxRy z Lz) Lv0u1 L6 L3u1 L7.
Assume Hv1u1: v1 ∈ SNoR u1.
Apply L3u1imp to the current goal.
We will prove x * u1 + v0 * v1 < v0 * u1 + x * v1.
Apply IHy u1 (SNoR_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ IHy3 _.
An exact proof term for the current goal is IHy3 v0 Hv0 v1 Hv1u1.
Assume Hu1v1: u1 ∈ SNoL v1.
Apply L3u1imp to the current goal.
We will prove x * u1 + v0 * v1 < v0 * u1 + x * v1.
rewrite the current goal using add_SNo_com (x * u1) (v0 * v1) Lxu1 Lv0v1 (from left to right).
rewrite the current goal using add_SNo_com (v0 * u1) (x * v1) Lv0u1 Lxv1 (from left to right).
Apply IHy v1 (SNoR_SNoS y Hy v1 Hv1) to the current goal.
Assume _ IHy1 _ _ _.
An exact proof term for the current goal is IHy1 v0 Hv0 u1 Hu1v1.
Let v0 be given.
Assume Hv0.
Let v1 be given.
Assume Hv1 Hve.
Apply SNoR_E x Hx v0 Hv0 to the current goal.
Assume Hv0a: SNo v0.
Assume Hv0b: SNoLev v0 ∈ SNoLev x.
Assume Hv0c: x < v0.
Apply SNoL_E y Hy v1 Hv1 to the current goal.
Assume Hv1a: SNo v1.
Assume Hv1b: SNoLev v1 ∈ SNoLev y.
Assume Hv1c: v1 < y.
Apply Luvimp u0 (SNoR_SNoS x Hx u0 Hu0) v0 (SNoR_SNoS x Hx v0 Hv0) u1 (SNoR_SNoS y Hy u1 Hu1) v1 (SNoL_SNoS y Hy v1 Hv1) to the current goal.
Assume Lu0y Lxu1 Lu0u1 Lv0y Lxv1 Lv0v1 Lu0v1 Lv0u1 Luv.
Apply Luv Hue Hve to the current goal.
We will prove u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
We prove the intermediate claim Lv1u1lt: v1 < u1.
An exact proof term for the current goal is SNoLt_tra v1 y u1 Hv1a Hy Hu1a Hv1c Hu1c.
We prove the intermediate claim L3: ∀z ∈ SNoR x, x * u1 + z * v1 < z * u1 + x * v1.
Let z be given.
Assume Hz.
We prove the intermediate claim Lzu1: SNo (z * u1).
An exact proof term for the current goal is LRx z Hz u1 Hu1a.
We prove the intermediate claim Lzv1: SNo (z * v1).
An exact proof term for the current goal is LRx z Hz v1 Hv1a.
Apply SNoLt_SNoL_or_SNoR_impred v1 u1 Hv1a Hu1a Lv1u1lt to the current goal.
Let w be given.
Assume Hwu1: w ∈ SNoL u1.
Assume Hwv1: w ∈ SNoR v1.
Apply SNoL_E u1 Hu1a w Hwu1 to the current goal.
Assume Hwu1a: SNo w.
Assume Hwu1b: SNoLev w ∈ SNoLev u1.
Assume Hwu1c: w < u1.
We prove the intermediate claim LwSy: w ∈ SNoS_ (SNoLev y).
Apply SNoS_I2 w y Hwu1a Hy to the current goal.
We will prove SNoLev w ∈ SNoLev y.
An exact proof term for the current goal is ordinal_TransSet (SNoLev y) (SNoLev_ordinal y Hy) (SNoLev u1) Hu1b (SNoLev w) Hwu1b.
We prove the intermediate claim Lzw: SNo (z * w).
An exact proof term for the current goal is LRx z Hz w Hwu1a.
We prove the intermediate claim Lxw: SNo (x * w).
Apply IHy w LwSy to the current goal.
Assume H1 _ _ _ _.
An exact proof term for the current goal is H1.
We prove the intermediate claim L3a: z * v1 + x * w < x * v1 + z * w.
Apply IHy v1 (SNoL_SNoS y Hy v1 Hv1) to the current goal.
Assume _ _ IHy2 _ _.
An exact proof term for the current goal is IHy2 z Hz w Hwv1.
We prove the intermediate claim L3b: x * u1 + z * w < z * u1 + x * w.
Apply IHy u1 (SNoR_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ _ IHy4.
An exact proof term for the current goal is IHy4 z Hz w Hwu1.
An exact proof term for the current goal is add_SNo_Lt_subprop2 (x * u1) (z * v1) (z * u1) (x * v1) (z * w) (x * w) Lxu1 Lzv1 Lzu1 Lxv1 Lzw Lxw L3b L3a.
Assume Hv1u1: v1 ∈ SNoL u1.
Apply IHy u1 (SNoR_SNoS y Hy u1 Hu1) to the current goal.
Assume _ _ _ _ IHy4.
An exact proof term for the current goal is IHy4 z Hz v1 Hv1u1.
Assume Hu1v1: u1 ∈ SNoR v1.
Apply IHy v1 (SNoL_SNoS y Hy v1 Hv1) to the current goal.
Assume _ _ IHy2 _ _.
rewrite the current goal using add_SNo_com (x * u1) (z * v1) Lxu1 Lzv1 (from left to right).
rewrite the current goal using add_SNo_com (z * u1) (x * v1) Lzu1 Lxv1 (from left to right).
We will prove z * v1 + x * u1 < x * v1 + z * u1.
An exact proof term for the current goal is IHy2 z Hz u1 Hu1v1.
We prove the intermediate claim L3u0: x * u1 + u0 * v1 < u0 * u1 + x * v1.
An exact proof term for the current goal is L3 u0 Hu0.
We prove the intermediate claim L3v0: x * u1 + v0 * v1 < v0 * u1 + x * v1.
An exact proof term for the current goal is L3 v0 Hv0.
We prove the intermediate claim L3u0imp: u0 * y + v0 * v1 < v0 * y + u0 * v1 → u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
Assume H1.
Apply add_SNo_Lt_subprop3a (u0 * y) (x * u1) (v0 * v1) (v0 * y) (x * v1 + u0 * u1) (u0 * v1) Lu0y Lxu1 Lv0v1 Lv0y (SNo_add_SNo (x * v1) (u0 * u1) Lxv1 Lu0u1) Lu0v1 H1 to the current goal.
We will prove x * u1 + u0 * v1 < x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com (x * v1) (u0 * u1) Lxv1 Lu0u1 (from left to right).
An exact proof term for the current goal is L3u0.
We prove the intermediate claim L3v0imp: u0 * y + v0 * u1 < v0 * y + u0 * u1 → u0 * y + x * u1 + v0 * v1 < v0 * y + x * v1 + u0 * u1.
Assume H1.
Apply add_SNo_Lt_subprop3b (u0 * y) (x * u1 + v0 * v1) (v0 * y) (x * v1) (u0 * u1) (v0 * u1) Lu0y (SNo_add_SNo (x * u1) (v0 * v1) Lxu1 Lv0v1) Lv0y Lxv1 Lu0u1 Lv0u1 to the current goal.
We will prove u0 * y + v0 * u1 < v0 * y + u0 * u1.
An exact proof term for the current goal is H1.
We will prove x * u1 + v0 * v1 < v0 * u1 + x * v1.
An exact proof term for the current goal is L3v0.
Apply SNoL_or_SNoR_impred v0 u0 Hv0a Hu0a to the current goal.
Assume Hv0u0: v0 = u0.
rewrite the current goal using Hv0u0 (from left to right).
We will prove u0 * y + (x * u1 + u0 * v1) < u0 * y + (x * v1 + u0 * u1).
Apply add_SNo_Lt2 (u0 * y) (x * u1 + u0 * v1) (x * v1 + u0 * u1) Lu0y (SNo_add_SNo (x * u1) (u0 * v1) Lxu1 Lu0v1) (SNo_add_SNo (x * v1) (u0 * u1) Lxv1 Lu0u1) to the current goal.
We will prove x * u1 + u0 * v1 < x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com (x * v1) (u0 * u1) Lxv1 Lu0u1 (from left to right).
An exact proof term for the current goal is L3u0.
Let z be given.
Assume Hzu0: z ∈ SNoL u0.
Assume Hzv0: z ∈ SNoR v0.
Apply SNoR_E v0 Hv0a z Hzv0 to the current goal.
Assume Hza: SNo z.
Assume Hzb: SNoLev z ∈ SNoLev v0.
Assume Hzc: v0 < z.
We prove the intermediate claim Lz: z ∈ SNoR x.
Apply SNoR_I x Hx z Hza to the current goal.
We will prove SNoLev z ∈ SNoLev x.
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) (SNoLev v0) Hv0b (SNoLev z) Hzb.
We will prove x < z.
An exact proof term for the current goal is SNoLt_tra x v0 z Hx Hv0a Hza Hv0c Hzc.
We prove the intermediate claim L4: u0 * y + z * u1 < z * y + u0 * u1.
Apply IHx u0 (SNoR_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ IHx3 _.
An exact proof term for the current goal is IHx3 z Hzu0 u1 Hu1.
We prove the intermediate claim L5: z * y + v0 * u1 < v0 * y + z * u1.
Apply IHx v0 (SNoR_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ _ IHx2 _ _.
An exact proof term for the current goal is IHx2 z Hzv0 u1 Hu1.
An exact proof term for the current goal is add_SNo_Lt_subprop3d (u0 * y) (x * u1 + v0 * v1) (v0 * y) (x * v1) (u0 * u1) (z * u1) (z * y) (v0 * u1) Lu0y (SNo_add_SNo (x * u1) (v0 * v1) Lxu1 Lv0v1) Lv0y Lxv1 Lu0u1 (LRx z Lz u1 Hu1a) (LRxy z Lz) Lv0u1 L4 L3v0 L5.
Assume Hv0u0: v0 ∈ SNoL u0.
Apply L3v0imp to the current goal.
We will prove u0 * y + v0 * u1 < v0 * y + u0 * u1.
Apply IHx u0 (SNoR_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ IHx3 _.
An exact proof term for the current goal is IHx3 v0 Hv0u0 u1 Hu1.
Assume Hu0v0: u0 ∈ SNoR v0.
Apply L3v0imp to the current goal.
We will prove u0 * y + v0 * u1 < v0 * y + u0 * u1.
Apply IHx v0 (SNoR_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ _ IHx2 _ _.
An exact proof term for the current goal is IHx2 u0 Hu0v0 u1 Hu1.
Let z be given.
Assume Hzu0: z ∈ SNoR u0.
Assume Hzv0: z ∈ SNoL v0.
Apply SNoR_E u0 Hu0a z Hzu0 to the current goal.
Assume Hza: SNo z.
Assume Hzb: SNoLev z ∈ SNoLev u0.
Assume Hzc: u0 < z.
We prove the intermediate claim Lz: z ∈ SNoR x.
Apply SNoR_I x Hx z Hza to the current goal.
We will prove SNoLev z ∈ SNoLev x.
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) (SNoLev u0) Hu0b (SNoLev z) Hzb.
We will prove x < z.
An exact proof term for the current goal is SNoLt_tra x u0 z Hx Hu0a Hza Hu0c Hzc.
We prove the intermediate claim L6: u0 * y + z * v1 < z * y + u0 * v1.
Apply IHx u0 (SNoR_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ _ IHx4.
An exact proof term for the current goal is IHx4 z Hzu0 v1 Hv1.
We prove the intermediate claim L7: z * y + v0 * v1 < v0 * y + z * v1.
Apply IHx v0 (SNoR_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ IHx1 _ _ _.
An exact proof term for the current goal is IHx1 z Hzv0 v1 Hv1.
Apply add_SNo_Lt_subprop3c (u0 * y) (x * u1) (v0 * v1) (v0 * y) (x * v1 + u0 * u1) (z * v1) (z * y) (u0 * v1) Lu0y Lxu1 Lv0v1 Lv0y (SNo_add_SNo (x * v1) (u0 * u1) Lxv1 Lu0u1) (LRx z Lz v1 Hv1a) (LRxy z Lz) Lu0v1 L6 to the current goal.
We will prove x * u1 + u0 * v1 < x * v1 + u0 * u1.
rewrite the current goal using add_SNo_com (x * v1) (u0 * u1) Lxv1 Lu0u1 (from left to right).
An exact proof term for the current goal is L3u0.
We will prove z * y + v0 * v1 < v0 * y + z * v1.
An exact proof term for the current goal is L7.
Assume Hv0u0: v0 ∈ SNoR u0.
Apply L3u0imp to the current goal.
We will prove u0 * y + v0 * v1 < v0 * y + u0 * v1.
Apply IHx u0 (SNoR_SNoS x Hx u0 Hu0) y Hy to the current goal.
Assume _ _ _ _ IHx4.
An exact proof term for the current goal is IHx4 v0 Hv0u0 v1 Hv1.
Assume Hu0v0: u0 ∈ SNoL v0.
Apply L3u0imp to the current goal.
We will prove u0 * y + v0 * v1 < v0 * y + u0 * v1.
Apply IHx v0 (SNoR_SNoS x Hx v0 Hv0) y Hy to the current goal.
Assume _ IHx1 _ _ _.
An exact proof term for the current goal is IHx1 u0 Hu0v0 v1 Hv1.
We prove the intermediate claim Lxy: SNo (x * y).
rewrite the current goal using Hxy (from left to right).
We will prove SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R LLR1.
Let p be given.
Assume Hp.
We will prove p.
Apply Hp to the current goal.
An exact proof term for the current goal is Lxy.
We will prove ∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
We will prove u * y + x * v < x * y + u * v.
We prove the intermediate claim L1: u * y + x * v + - u * v < x * y.
rewrite the current goal using Hxy (from left to right).
We will prove u * y + x * v + - u * v < SNoCut L R.
Apply SNoCutP_SNoCut_L L R LLR1 to the current goal.
We will prove u * y + x * v + - u * v ∈ L.
An exact proof term for the current goal is HLI1 u Hu v Hv.
Apply add_SNo_minus_Lt1 (u * y + x * v) (u * v) (x * y) to the current goal.
An exact proof term for the current goal is SNo_add_SNo (u * y) (x * v) (LLx u Hu y Hy) (LxLy v Hv).
An exact proof term for the current goal is LLx u Hu v Hva.
An exact proof term for the current goal is Lxy.
We will prove (u * y + x * v) + - u * v < x * y.
rewrite the current goal using add_SNo_assoc (u * y) (x * v) (- (u * v)) (LLx u Hu y Hy) (LxLy v Hv) (SNo_minus_SNo (u * v) (LLx u Hu v Hva)) (from right to left).
An exact proof term for the current goal is L1.
We will prove ∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
We will prove u * y + x * v < x * y + u * v.
We prove the intermediate claim L1: u * y + x * v + - u * v < x * y.
rewrite the current goal using Hxy (from left to right).
We will prove u * y + x * v + - u * v < SNoCut L R.
Apply SNoCutP_SNoCut_L L R LLR1 to the current goal.
We will prove u * y + x * v + - u * v ∈ L.
An exact proof term for the current goal is HLI2 u Hu v Hv.
Apply add_SNo_minus_Lt1 (u * y + x * v) (u * v) (x * y) to the current goal.
An exact proof term for the current goal is SNo_add_SNo (u * y) (x * v) (LRx u Hu y Hy) (LxRy v Hv).
An exact proof term for the current goal is LRx u Hu v Hva.
An exact proof term for the current goal is Lxy.
We will prove (u * y + x * v) + - u * v < x * y.
rewrite the current goal using add_SNo_assoc (u * y) (x * v) (- (u * v)) (LRx u Hu y Hy) (LxRy v Hv) (SNo_minus_SNo (u * v) (LRx u Hu v Hva)) (from right to left).
An exact proof term for the current goal is L1.
We will prove ∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
We will prove x * y + u * v < u * y + x * v.
We prove the intermediate claim L1: x * y < u * y + x * v + - u * v.
rewrite the current goal using Hxy (from left to right).
We will prove SNoCut L R < u * y + x * v + - u * v.
Apply SNoCutP_SNoCut_R L R LLR1 to the current goal.
We will prove u * y + x * v + - u * v ∈ R.
An exact proof term for the current goal is HRI1 u Hu v Hv.
Apply add_SNo_minus_Lt2 (u * y + x * v) (u * v) (x * y) to the current goal.
An exact proof term for the current goal is SNo_add_SNo (u * y) (x * v) (LLx u Hu y Hy) (LxRy v Hv).
An exact proof term for the current goal is LLx u Hu v Hva.
An exact proof term for the current goal is Lxy.
We will prove x * y < (u * y + x * v) + - u * v.
rewrite the current goal using add_SNo_assoc (u * y) (x * v) (- (u * v)) (LLx u Hu y Hy) (LxRy v Hv) (SNo_minus_SNo (u * v) (LLx u Hu v Hva)) (from right to left).
An exact proof term for the current goal is L1.
We will prove ∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
We will prove x * y + u * v < u * y + x * v.
We prove the intermediate claim L1: x * y < u * y + x * v + - u * v.
rewrite the current goal using Hxy (from left to right).
We will prove SNoCut L R < u * y + x * v + - u * v.
Apply SNoCutP_SNoCut_R L R LLR1 to the current goal.
We will prove u * y + x * v + - u * v ∈ R.
An exact proof term for the current goal is HRI2 u Hu v Hv.
Apply add_SNo_minus_Lt2 (u * y + x * v) (u * v) (x * y) to the current goal.
An exact proof term for the current goal is SNo_add_SNo (u * y) (x * v) (LRx u Hu y Hy) (LxLy v Hv).
An exact proof term for the current goal is LRx u Hu v Hva.
An exact proof term for the current goal is Lxy.
We will prove x * y < (u * y + x * v) + - u * v.
rewrite the current goal using add_SNo_assoc (u * y) (x * v) (- (u * v)) (LRx u Hu y Hy) (LxLy v Hv) (SNo_minus_SNo (u * v) (LRx u Hu v Hva)) (from right to left).
An exact proof term for the current goal is L1.
∎