Object. The name In is a term of type set → set → prop.
Notation. We use ∈ as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write ∀ x ∈ A, B to mean ∀ x : set, x ∈ A → B.
Definition. We define Subq to be λA B ⇒ ∀x ∈ A, x ∈ B of type set → set → prop.
Notation. We use ⊆ as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write ∀ x ⊆ A, B to mean ∀ x : set, x ⊆ A → B.
Axiom. (set_ext) We take the following as an axiom:
∀X Y : set, X ⊆ Y → Y ⊆ X → X = Y
Axiom. (In_ind) We take the following as an axiom:
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.
Definition. We define SetAdjoin to be λX y ⇒ X ∪ {y} of type set → set → set.
Notation. We now use the set enumeration notation {...,...,...} in general. If 0 elements are given, then Empty is used to form the corresponding term. If 1 element is given, then Sing is used to form the corresponding term. If 2 elements are given, then UPair is used to form the corresponding term. If more than elements are given, then SetAdjoin is used to reduce to the case with one fewer elements.
Object. The name famunion is a term of type set → (set → set) → set.
Notation. We use ⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using famunion.
Axiom. (famunionI) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀x y : set, x ∈ X → y ∈ Fx → y ∈ ⋃x ∈ XFx
Axiom. (famunionE) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XFx) → ∃x ∈ X, y ∈ Fx
Definition. We define inj to be λX Y f ⇒ (∀u ∈ X, fu ∈ Y) ∧ (∀u v ∈ X, fu = fv → u = v) of type set → set → (set → set) → prop.
Definition. We define bij to be λX Y f ⇒ (∀u ∈ X, fu ∈ Y) ∧ (∀u v ∈ X, fu = fv → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, fu = w) of type set → set → (set → set) → prop.
Definition. We define PNoLe to be λalpha p beta q ⇒ PNoLtalphapbetaq ∨ alpha = beta ∧ PNoEq_alphapq of type set → (set → prop) → set → (set → prop) → prop.
Axiom. (PNoLeI1) We take the following as an axiom:
Definition. We define PNo_downc to be λL alpha p ⇒ ∃beta, ordinalbeta ∧ ∃q : set → prop, Lbetaq ∧ PNoLealphapbetaq of type (set → (set → prop) → prop) → set → (set → prop) → prop.
Definition. We define PNo_upc to be λR alpha p ⇒ ∃beta, ordinalbeta ∧ ∃q : set → prop, Rbetaq ∧ PNoLebetaqalphap of type (set → (set → prop) → prop) → set → (set → prop) → prop.
Axiom. (PNoLe_downc) We take the following as an axiom:
Definition. We define PNo_rel_strict_upperbd to be λL alpha p ⇒ ∀beta ∈ alpha, ∀q : set → prop, PNo_downcLbetaq → PNoLtbetaqalphap of type (set → (set → prop) → prop) → set → (set → prop) → prop.
Definition. We define PNo_rel_strict_lowerbd to be λR alpha p ⇒ ∀beta ∈ alpha, ∀q : set → prop, PNo_upcRbetaq → PNoLtalphapbetaq of type (set → (set → prop) → prop) → set → (set → prop) → prop.
Definition. We define PNo_strict_upperbd to be λL alpha p ⇒ ∀beta, ordinalbeta → ∀q : set → prop, Lbetaq → PNoLtbetaqalphap of type (set → (set → prop) → prop) → set → (set → prop) → prop.
Definition. We define PNo_strict_lowerbd to be λR alpha p ⇒ ∀beta, ordinalbeta → ∀q : set → prop, Rbetaq → PNoLtalphapbetaq of type (set → (set → prop) → prop) → set → (set → prop) → prop.
Definition. We define PNo_strict_imv to be λL R alpha p ⇒ PNo_strict_upperbdLalphap ∧ PNo_strict_lowerbdRalphap of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
Definition. We define PNo_least_rep to be λL R beta p ⇒ ordinalbeta ∧ PNo_strict_imvLRbetap ∧ ∀gamma ∈ beta, ∀q : set → prop, ¬ PNo_strict_imvLRgammaq of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
Definition. We define PNo_least_rep2 to be λL R beta p ⇒ PNo_least_repLRbetap ∧ ∀x, x ∉ beta → ¬ px of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
LetG : set → (set → set → set) → set → set ≝ λalpha g ⇒ If_ii(ordinalalpha)(λz : set ⇒ ifz ∈ SNoS_(ordsuccalpha)thenFz(λw ⇒ g(SNoLevw)w)elsedefault)(λz : set ⇒ default)
Object. The name SNo_rec_i is a term of type set → set.
∀x, SNox → ∀y, SNoy → ∀p : prop, (SNo(x * y) → (∀u ∈ SNoLx, ∀v ∈ SNoLy, u * y + x * v < x * y + u * v) → (∀u ∈ SNoRx, ∀v ∈ SNoRy, u * y + x * v < x * y + u * v) → (∀u ∈ SNoLx, ∀v ∈ SNoRy, x * y + u * v < u * y + x * v) → (∀u ∈ SNoRx, ∀v ∈ SNoLy, x * y + u * v < u * y + x * v) → p) → p
Proof:
SetP to be the term λx ⇒ ∀y, SNoy → ∀p : prop, (SNo(x * y) → (∀u ∈ SNoLx, ∀v ∈ SNoLy, u * y + x * v < x * y + u * v) → (∀u ∈ SNoRx, ∀v ∈ SNoRy, u * y + x * v < x * y + u * v) → (∀u ∈ SNoLx, ∀v ∈ SNoRy, x * y + u * v < u * y + x * v) → (∀u ∈ SNoRx, ∀v ∈ SNoLy, x * y + u * v < u * y + x * v) → p) → p of type set → prop.
SetQ to be the term λy ⇒ ∀p : prop, (SNo(x * y) → (∀u ∈ SNoLx, ∀v ∈ SNoLy, u * y + x * v < x * y + u * v) → (∀u ∈ SNoRx, ∀v ∈ SNoRy, u * y + x * v < x * y + u * v) → (∀u ∈ SNoLx, ∀v ∈ SNoRy, x * y + u * v < u * y + x * v) → (∀u ∈ SNoRx, ∀v ∈ SNoLy, x * y + u * v < u * y + x * v) → p) → p of type set → prop.
ApplyIHxu0(SNoL_SNoSxHxu0Hu0)yHy to the current goal.
Assume_ _ _ _ IHx4.
An exact proof term for the current goal is IHx4v0Hv0u0zHz.
We prove the intermediate claimL3u1: u0 * y + v0 * u1 < v0 * y + u0 * u1.
An exact proof term for the current goal is L3u1Hu1.
We prove the intermediate claimL3v1: u0 * y + v0 * v1 < v0 * y + u0 * v1.
An exact proof term for the current goal is L3v1Hv1.
We prove the intermediate claimL3u1imp: 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)Lxu1Lv0v1)Lv0yLxv1Lu0u1Lv0u1L3u1.
We prove the intermediate claimL3v1imp: 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)Lu0yLxu1Lv0v1Lv0y(SNo_add_SNo(x * v1)(u0 * u1)Lxv1Lu0u1)Lu0v1L3v1.
An exact proof term for the current goal is SNoLt_trazu1yHzaHu1aHyHzcHu1c.
We prove the intermediate claimL4: x * u1 + v0 * z < x * z + v0 * u1.
rewrite the current goal using add_SNo_com(x * z)(v0 * u1)(LxLyzLz)Lv0u1 (from left to right).
We will provex * u1 + v0 * z < v0 * u1 + x * z.
ApplyIHyu1(SNoL_SNoSyHyu1Hu1) to the current goal.
Assume_ _ _ _ IHy4.
An exact proof term for the current goal is IHy4v0Hv0zHzu1.
We prove the intermediate claimL5: x * z + v0 * v1 < x * v1 + v0 * z.
rewrite the current goal using add_SNo_com(x * z)(v0 * v1)(LxLyzLz)Lv0v1 (from left to right).
ApplyIHyv1(SNoL_SNoSyHyv1Hv1) to the current goal.
Assume_ _ IHy2 _ _.
An exact proof term for the current goal is IHy2v0Hv0zHzv1.
We will proveu0 * 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)Lu0yLxu1Lv0v1 (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(v0 * y)(x * v1)(u0 * u1)Lv0yLxv1Lu0u1 (from left to right).
We will provex * 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)Lxu1Lu0yLv0v1Lxv1(SNo_add_SNo(v0 * y)(u0 * u1)Lv0yLu0u1)(LRxv0Hv0zHza)(LxLyzLz)Lv0u1L4L3u1L5.
ApplyIHxv0(SNoL_SNoSxHxv0Hv0)yHy to the current goal.
Assume_ _ IHx2 _ _.
An exact proof term for the current goal is IHx2u0Hu0v0zHz.
We prove the intermediate claimL3u1: u0 * y + v0 * u1 < v0 * y + u0 * u1.
An exact proof term for the current goal is L3u1Hu1.
We prove the intermediate claimL3v1: u0 * y + v0 * v1 < v0 * y + u0 * v1.
An exact proof term for the current goal is L3v1Hv1.
We prove the intermediate claimL3u1imp: 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)Lxu1Lv0v1)Lv0yLxv1Lu0u1Lv0u1L3u1.
We prove the intermediate claimL3v1imp: 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)Lu0yLxu1Lv0v1Lv0y(SNo_add_SNo(x * v1)(u0 * u1)Lxv1Lu0u1)Lu0v1L3v1.
An exact proof term for the current goal is SNoLt_trayu1zHyHu1aHzaHu1cHzc.
We prove the intermediate claimL6: x * u1 + v0 * z < x * z + v0 * u1.
rewrite the current goal using add_SNo_com(x * z)(v0 * u1)(LxRyzLz)Lv0u1 (from left to right).
We will provex * u1 + v0 * z < v0 * u1 + x * z.
ApplyIHyu1(SNoR_SNoSyHyu1Hu1) to the current goal.
Assume_ _ _ IHy3 _.
An exact proof term for the current goal is IHy3v0Hv0zHzu1.
We prove the intermediate claimL7: x * z + v0 * v1 < x * v1 + v0 * z.
rewrite the current goal using add_SNo_com(x * z)(v0 * v1)(LxRyzLz)Lv0v1 (from left to right).
ApplyIHyv1(SNoR_SNoSyHyv1Hv1) to the current goal.
Assume_ IHy1 _ _ _.
An exact proof term for the current goal is IHy1v0Hv0zHzv1.
We will proveu0 * 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)Lu0yLxu1Lv0v1 (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(v0 * y)(x * v1)(u0 * u1)Lv0yLxv1Lu0u1 (from left to right).
We will provex * 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)Lxu1Lu0yLv0v1Lxv1(SNo_add_SNo(v0 * y)(u0 * u1)Lv0yLu0u1)(LLxv0Hv0zHza)(LxRyzLz)Lv0u1L6L3u1L7.
An exact proof term for the current goal is SNo_mul_SNoxv'HxHv'a.
We prove the intermediate claimLu'v': SNo(u' * v').
An exact proof term for the current goal is SNo_mul_SNou'v'Hu'aHv'a.
rewrite the current goal using Hwe (from left to right).
rewrite the current goal using Hze (from left to right).
We will proveu * y + x * v + - u * v < u' * y + x * v' + - u' * v'.
Applyadd_SNo_minus_Lt_lem(u * y)(x * v)(u * v)(u' * y)(x * v')(u' * v')LuyLxvLuvLu'yLxv'Lu'v' to the current goal.
We will proveu * y + x * v + u' * v' < u' * y + x * v' + u * v.
ApplySNoLt_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')LuyLxvLu'v')(SNo_add_SNo_3(x * y)(u * v)(u' * v')HxyLuvLu'v')(SNo_add_SNo_3(u' * y)(x * v')(u * v)Lu'yLxv'Luv) to the current goal.
We will proveu * y + x * v + u' * v' < x * y + u * v + u' * v'.
Applyadd_SNo_3_3_3_Lt1(u * y)(x * v)(x * y)(u * v)(u' * v')LuyLxvHxyLuvLu'v' to the current goal.
We will proveu * y + x * v < x * y + u * v.
An exact proof term for the current goal is Hxy1uHuvHv.
We will provex * y + u * v + u' * v' < u' * y + x * v' + u * v.
Applyadd_SNo_3_2_3_Lt1(x * y)(u' * v')(u' * y)(x * v')(u * v)HxyLu'v'Lu'yLxv'Luv to the current goal.
We will proveu' * 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 Hxy3u'Hu'v'Hv'.
An exact proof term for the current goal is SNo_mul_SNoxv'HxHv'a.
We prove the intermediate claimLu'v': SNo(u' * v').
An exact proof term for the current goal is SNo_mul_SNou'v'Hu'aHv'a.
rewrite the current goal using Hwe (from left to right).
rewrite the current goal using Hze (from left to right).
We will proveu * y + x * v + - u * v < u' * y + x * v' + - u' * v'.
Applyadd_SNo_minus_Lt_lem(u * y)(x * v)(u * v)(u' * y)(x * v')(u' * v')LuyLxvLuvLu'yLxv'Lu'v' to the current goal.
We will proveu * y + x * v + u' * v' < u' * y + x * v' + u * v.
ApplySNoLt_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')LuyLxvLu'v')(SNo_add_SNo_3(x * y)(u * v)(u' * v')HxyLuvLu'v')(SNo_add_SNo_3(u' * y)(x * v')(u * v)Lu'yLxv'Luv) to the current goal.
We will proveu * y + x * v + u' * v' < x * y + u * v + u' * v'.
Applyadd_SNo_3_3_3_Lt1(u * y)(x * v)(x * y)(u * v)(u' * v')LuyLxvHxyLuvLu'v' to the current goal.
We will proveu * y + x * v < x * y + u * v.
An exact proof term for the current goal is Hxy1uHuvHv.
We will provex * y + u * v + u' * v' < u' * y + x * v' + u * v.
Applyadd_SNo_3_2_3_Lt1(x * y)(u' * v')(u' * y)(x * v')(u * v)HxyLu'v'Lu'yLxv'Luv to the current goal.
We will proveu' * 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 Hxy4u'Hu'v'Hv'.
An exact proof term for the current goal is SNo_mul_SNoxv'HxHv'a.
We prove the intermediate claimLu'v': SNo(u' * v').
An exact proof term for the current goal is SNo_mul_SNou'v'Hu'aHv'a.
rewrite the current goal using Hwe (from left to right).
rewrite the current goal using Hze (from left to right).
We will proveu * y + x * v + - u * v < u' * y + x * v' + - u' * v'.
Applyadd_SNo_minus_Lt_lem(u * y)(x * v)(u * v)(u' * y)(x * v')(u' * v')LuyLxvLuvLu'yLxv'Lu'v' to the current goal.
We will proveu * y + x * v + u' * v' < u' * y + x * v' + u * v.
ApplySNoLt_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')LuyLxvLu'v')(SNo_add_SNo_3(x * y)(u * v)(u' * v')HxyLuvLu'v')(SNo_add_SNo_3(u' * y)(x * v')(u * v)Lu'yLxv'Luv) to the current goal.
We will proveu * y + x * v + u' * v' < x * y + u * v + u' * v'.
Applyadd_SNo_3_3_3_Lt1(u * y)(x * v)(x * y)(u * v)(u' * v')LuyLxvHxyLuvLu'v' to the current goal.
We will proveu * y + x * v < x * y + u * v.
An exact proof term for the current goal is Hxy2uHuvHv.
We will provex * y + u * v + u' * v' < u' * y + x * v' + u * v.
Applyadd_SNo_3_2_3_Lt1(x * y)(u' * v')(u' * y)(x * v')(u * v)HxyLu'v'Lu'yLxv'Luv to the current goal.
We will proveu' * 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 Hxy3u'Hu'v'Hv'.
An exact proof term for the current goal is SNo_mul_SNoxv'HxHv'a.
We prove the intermediate claimLu'v': SNo(u' * v').
An exact proof term for the current goal is SNo_mul_SNou'v'Hu'aHv'a.
rewrite the current goal using Hwe (from left to right).
rewrite the current goal using Hze (from left to right).
We will proveu * y + x * v + - u * v < u' * y + x * v' + - u' * v'.
Applyadd_SNo_minus_Lt_lem(u * y)(x * v)(u * v)(u' * y)(x * v')(u' * v')LuyLxvLuvLu'yLxv'Lu'v' to the current goal.
We will proveu * y + x * v + u' * v' < u' * y + x * v' + u * v.
ApplySNoLt_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')LuyLxvLu'v')(SNo_add_SNo_3(x * y)(u * v)(u' * v')HxyLuvLu'v')(SNo_add_SNo_3(u' * y)(x * v')(u * v)Lu'yLxv'Luv) to the current goal.
We will proveu * y + x * v + u' * v' < x * y + u * v + u' * v'.
Applyadd_SNo_3_3_3_Lt1(u * y)(x * v)(x * y)(u * v)(u' * v')LuyLxvHxyLuvLu'v' to the current goal.
We will proveu * y + x * v < x * y + u * v.
An exact proof term for the current goal is Hxy2uHuvHv.
We will provex * y + u * v + u' * v' < u' * y + x * v' + u * v.
Applyadd_SNo_3_2_3_Lt1(x * y)(u' * v')(u' * y)(x * v')(u * v)HxyLu'v'Lu'yLxv'Luv to the current goal.
We will proveu' * 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 Hxy4u'Hu'v'Hv'.
An exact proof term for the current goal is HpLRLLRHLEHLI1HLI2HREHRI1HRI2He.
An exact proof term for the current goal is SNo_mul_SNowzHw1Hz1.
We prove the intermediate claimL1: w * y + x * z < x * y + w * z.
An exact proof term for the current goal is Hxy1wLwxzLzy.
We prove the intermediate claimL2: w * v + u * z < u * v + w * z.
An exact proof term for the current goal is Huv2wLwuzLzv.
We prove the intermediate claimL3: x * v + w * z < w * v + x * z.
An exact proof term for the current goal is Hxv3wLwxzLzv.
We prove the intermediate claimL4: u * y + w * z < w * y + u * z.
An exact proof term for the current goal is Huy4wLwuzLzy.
We prove the intermediate claimLwzwz: SNo(w * z + w * z).
An exact proof term for the current goal is SNo_add_SNo(w * z)(w * z)LwzLwz.
Applyadd_SNo_Lt1_cancel(u * y + x * v)(w * z + w * z)(x * y + u * v)LuyxvLwzwzLxyuv to the current goal.
We will prove(u * y + x * v) + (w * z + w * z) < (x * y + u * v) + (w * z + w * z).
We prove the intermediate claimLwyuz: SNo(w * y + u * z).
An exact proof term for the current goal is SNo_add_SNo(w * y)(u * z)LwyLuz.
We prove the intermediate claimLwvxz: SNo(w * v + x * z).
An exact proof term for the current goal is SNo_add_SNo(w * v)(x * z)LwvLxz.
We prove the intermediate claimLuywz: SNo(u * y + w * z).
An exact proof term for the current goal is SNo_add_SNo(u * y)(w * z)HuyLwz.
We prove the intermediate claimLxvwz: SNo(x * v + w * z).
An exact proof term for the current goal is SNo_add_SNo(x * v)(w * z)HxvLwz.
We prove the intermediate claimLwvuz: SNo(w * v + u * z).
An exact proof term for the current goal is SNo_add_SNo(w * v)(u * z)LwvLuz.
We prove the intermediate claimLxyxz: SNo(x * y + x * z).
An exact proof term for the current goal is SNo_add_SNo(x * y)(x * z)HxyLxz.
We prove the intermediate claimLwyxz: SNo(w * y + x * z).
An exact proof term for the current goal is SNo_add_SNo(w * y)(x * z)LwyLxz.
We prove the intermediate claimLxywz: SNo(x * y + w * z).
An exact proof term for the current goal is SNo_add_SNo(x * y)(w * z)HxyLwz.
We prove the intermediate claimLuvwz: SNo(u * v + w * z).
An exact proof term for the current goal is SNo_add_SNo(u * v)(w * z)HuvLwz.
ApplySNoLt_tra((u * y + x * v) + (w * z + w * z))((w * y + u * z) + (w * v + x * z))((x * y + u * v) + (w * z + w * z))(SNo_add_SNo(u * y + x * v)(w * z + w * z)LuyxvLwzwz)(SNo_add_SNo(w * y + u * z)(w * v + x * z)LwyuzLwvxz)(SNo_add_SNo(x * y + u * v)(w * z + w * z)LxyuvLwzwz) to the current goal.
We will prove(u * y + x * v) + (w * z + w * z) < (w * y + u * z) + (w * v + x * z).
rewrite the current goal using add_SNo_com_4_inner_mid(u * y)(x * v)(w * z)(w * z)HuyHxvLwzLwz (from left to right).
We will prove(u * y + w * z) + (x * v + w * z) < (w * y + u * z) + (w * v + x * z).
Applyadd_SNo_Lt3(u * y + w * z)(x * v + w * z)(w * y + u * z)(w * v + x * z)LuywzLxvwzLwyuzLwvxz to the current goal.
We will proveu * y + w * z < w * y + u * z.
An exact proof term for the current goal is L4.
We will provex * v + w * z < w * v + x * z.
An exact proof term for the current goal is L3.
We will prove(w * y + u * z) + (w * v + x * z) < (x * y + u * v) + (w * z + w * z).
rewrite the current goal using add_SNo_com_4_inner_mid(x * y)(u * v)(w * z)(w * z)HxyHuvLwzLwz (from left to right).
We will prove(w * y + u * z) + (w * v + x * z) < (x * y + w * z) + (u * v + w * z).
rewrite the current goal using add_SNo_com(w * y)(u * z)LwyLuz (from left to right).
rewrite the current goal using add_SNo_com_4_inner_mid(u * z)(w * y)(w * v)(x * z)LuzLwyLwvLxz (from left to right).
rewrite the current goal using add_SNo_com(w * v)(u * z)LwvLuz (from right to left).
We will prove(w * v + u * z) + (w * y + x * z) < (x * y + w * z) + (u * v + w * z).
rewrite the current goal using add_SNo_com(w * v + u * z)(w * y + x * z)LwvuzLwyxz (from left to right).
We will prove(w * y + x * z) + (w * v + u * z) < (x * y + w * z) + (u * v + w * z).
Applyadd_SNo_Lt3(w * y + x * z)(w * v + u * z)(x * y + w * z)(u * v + w * z)LwyxzLwvuzLxywzLuvwz to the current goal.
An exact proof term for the current goal is SNoL_IyHyvHvH4Hvy.
We prove the intermediate claimL1: w * y + x * v < x * y + w * v.
An exact proof term for the current goal is Hxy1wLwxvLvy.
We prove the intermediate claimL2: u * y + w * v < w * y + u * v.
An exact proof term for the current goal is Huy4wLwuvLvy.
We will proveu * y + x * v < x * y + u * v.
Applyadd_SNo_Lt2_cancel(w * y)(u * y + x * v)(x * y + u * v)LwyLuyxvLxyuv to the current goal.
We will provew * y + u * y + x * v < w * y + x * y + u * v.
ApplySNoLt_tra(w * y + u * y + x * v)(u * y + w * v + x * y)(w * y + x * y + u * v)(SNo_add_SNo(w * y)(u * y + x * v)LwyLuyxv)(SNo_add_SNo(u * y)(w * v + x * y)Huy(SNo_add_SNo(w * v)(x * y)LwvHxy))(SNo_add_SNo(w * y)(x * y + u * v)LwyLxyuv) to the current goal.
We will provew * y + u * y + x * v < u * y + w * v + x * y.
rewrite the current goal using add_SNo_com_3_0_1(w * y)(u * y)(x * v)LwyHuyHxv (from left to right).
We will proveu * y + w * y + x * v < u * y + w * v + x * y.
rewrite the current goal using add_SNo_com(w * v)(x * y)LwvHxy (from left to right).
An exact proof term for the current goal is add_SNo_Lt2(u * y)(w * y + x * v)(x * y + w * v)HuyLwyxvLxywvL1.
We will proveu * y + w * v + x * y < w * y + x * y + u * v.
rewrite the current goal using add_SNo_assoc(u * y)(w * v)(x * y)HuyLwvHxy (from left to right).
We will prove(u * y + w * v) + x * y < w * y + x * y + u * v.
rewrite the current goal using add_SNo_com(x * y)(u * v)HxyHuv (from left to right).
We will prove(u * y + w * v) + x * y < w * y + u * v + x * y.
rewrite the current goal using add_SNo_assoc(w * y)(u * v)(x * y)LwyHuvHxy (from left to right).
We will prove(u * y + w * v) + x * y < (w * y + u * v) + x * y.
An exact proof term for the current goal is add_SNo_Lt1(u * y + w * v)(x * y)(w * y + u * v)LuywvHxyLwyuvL2.
An exact proof term for the current goal is SNoR_IvHvyHyH4Hvy.
We prove the intermediate claimL1: x * v + w * y < w * v + x * y.
An exact proof term for the current goal is Hxv3wLwxyLyv.
We prove the intermediate claimL2: w * v + u * y < u * v + w * y.
An exact proof term for the current goal is Huv2wLwuyLyv.
We will proveu * y + x * v < x * y + u * v.
Applyadd_SNo_Lt2_cancel(w * y)(u * y + x * v)(x * y + u * v)LwyLuyxvLxyuv to the current goal.
We will provew * y + u * y + x * v < w * y + x * y + u * v.
ApplySNoLt_tra(w * y + u * y + x * v)(u * y + w * v + x * y)(w * y + x * y + u * v)(SNo_add_SNo(w * y)(u * y + x * v)LwyLuyxv)(SNo_add_SNo(u * y)(w * v + x * y)Huy(SNo_add_SNo(w * v)(x * y)LwvHxy))(SNo_add_SNo(w * y)(x * y + u * v)LwyLxyuv) to the current goal.
We will provew * y + u * y + x * v < u * y + w * v + x * y.
rewrite the current goal using add_SNo_rotate_3_1(u * y)(x * v)(w * y)HuyHxvLwy (from right to left).
We will proveu * y + x * v + w * y < u * y + w * v + x * y.
An exact proof term for the current goal is add_SNo_Lt2(u * y)(x * v + w * y)(w * v + x * y)HuyLxvwyLwvxyL1.
We will proveu * y + w * v + x * y < w * y + x * y + u * v.
rewrite the current goal using add_SNo_rotate_3_1(w * y)(x * y)(u * v)LwyHxyHuv (from left to right).
We will proveu * y + w * v + x * y < u * v + w * y + x * y.
rewrite the current goal using add_SNo_assoc(u * y)(w * v)(x * y)HuyLwvHxy (from left to right).
rewrite the current goal using add_SNo_assoc(u * v)(w * y)(x * y)HuvLwyHxy (from left to right).
We will prove(u * y + w * v) + x * y < (u * v + w * y) + x * y.
rewrite the current goal using add_SNo_com(u * y)(w * v)HuyLwv (from left to right).
We will prove(w * v + u * y) + x * y < (u * v + w * y) + x * y.
Applyadd_SNo_Lt1(w * v + u * y)(x * y)(u * v + w * y)LwvuyHxyLuvwyL2 to the current goal.
An exact proof term for the current goal is SNo_mul_SNouzHuHz1.
We prove the intermediate claimLuyxz: SNo(u * y + x * z).
An exact proof term for the current goal is SNo_add_SNo(u * y)(x * z)HuyLxz.
We prove the intermediate claimLuvxz: SNo(u * v + x * z).
An exact proof term for the current goal is SNo_add_SNo(u * v)(x * z)HuvLxz.
We prove the intermediate claimLxyuz: SNo(x * y + u * z).
An exact proof term for the current goal is SNo_add_SNo(x * y)(u * z)HxyLuz.
We prove the intermediate claimLxvuz: SNo(x * v + u * z).
An exact proof term for the current goal is SNo_add_SNo(x * v)(u * z)HxvLuz.
We prove the intermediate claimL1: u * y + x * z < x * y + u * z.
An exact proof term for the current goal is Hxy1uLuxzLzy.
We prove the intermediate claimL2: x * v + u * z < u * v + x * z.
An exact proof term for the current goal is Hxv3uLuxzLzv.
We will proveu * y + x * v < x * y + u * v.
Applyadd_SNo_Lt2_cancel(x * z)(u * y + x * v)(x * y + u * v)LxzLuyxvLxyuv to the current goal.
We will provex * z + u * y + x * v < x * z + x * y + u * v.
ApplySNoLt_tra(x * z + u * y + x * v)(x * y + u * z + x * v)(x * z + x * y + u * v)(SNo_add_SNo(x * z)(u * y + x * v)LxzLuyxv)(SNo_add_SNo(x * y)(u * z + x * v)Hxy(SNo_add_SNo(u * z)(x * v)LuzHxv))(SNo_add_SNo(x * z)(x * y + u * v)LxzLxyuv) to the current goal.
We will provex * z + u * y + x * v < x * y + u * z + x * v.
rewrite the current goal using add_SNo_assoc(x * z)(u * y)(x * v)LxzHuyHxv (from left to right).
rewrite the current goal using add_SNo_com(x * z)(u * y)LxzHuy (from left to right).
We will prove(u * y + x * z) + x * v < x * y + u * z + x * v.
rewrite the current goal using add_SNo_assoc(x * y)(u * z)(x * v)HxyLuzHxv (from left to right).
An exact proof term for the current goal is add_SNo_Lt1(u * y + x * z)(x * v)(x * y + u * z)LuyxzHxvLxyuzL1.
We will provex * y + u * z + x * v < x * z + x * y + u * v.
rewrite the current goal using add_SNo_rotate_3_1(x * y)(u * v)(x * z)HxyHuvLxz (from right to left).
We will provex * y + u * z + x * v < x * y + u * v + x * z.
rewrite the current goal using add_SNo_com(u * z)(x * v)LuzHxv (from left to right).
We will provex * y + x * v + u * z < x * y + u * v + x * z.
An exact proof term for the current goal is add_SNo_Lt2(x * y)(x * v + u * z)(u * v + x * z)HxyLxvuzLuvxzL2.
An exact proof term for the current goal is SNo_mul_SNouzHuHz1.
We prove the intermediate claimL1: u * y + x * z < x * y + u * z.
An exact proof term for the current goal is Huy4xLxuzLzy.
We prove the intermediate claimL2: x * v + u * z < u * v + x * z.
An exact proof term for the current goal is Huv2xLxuzLzv.
We will proveu * y + x * v < x * y + u * v.
Applyadd_SNo_Lt1_cancel(u * y + x * v)(x * z)(x * y + u * v)LuyxvLxzLxyuv to the current goal.
We will prove(u * y + x * v) + x * z < (x * y + u * v) + x * z.
rewrite the current goal using add_SNo_com(u * y)(x * v)HuyHxv (from left to right).
We will prove(x * v + u * y) + x * z < (x * y + u * v) + x * z.
rewrite the current goal using add_SNo_assoc(x * v)(u * y)(x * z)HxvHuyLxz (from right to left).
rewrite the current goal using add_SNo_assoc(x * y)(u * v)(x * z)HxyHuvLxz (from right to left).
We will provex * v + u * y + x * z < x * y + u * v + x * z.
We prove the intermediate claimLuyxz: SNo(u * y + x * z).
An exact proof term for the current goal is SNo_add_SNo(u * y)(x * z)HuyLxz.
We prove the intermediate claimLuzxy: SNo(u * z + x * y).
An exact proof term for the current goal is SNo_add_SNo(u * z)(x * y)LuzHxy.
We prove the intermediate claimLuvxz: SNo(u * v + x * z).
An exact proof term for the current goal is SNo_add_SNo(u * v)(x * z)HuvLxz.
ApplySNoLt_tra(x * v + u * y + x * z)(x * v + u * z + x * y)(x * y + u * v + x * z)(SNo_add_SNo(x * v)(u * y + x * z)HxvLuyxz)(SNo_add_SNo(x * v)(u * z + x * y)HxvLuzxy)(SNo_add_SNo(x * y)(u * v + x * z)HxyLuvxz) to the current goal.
We will provex * v + u * y + x * z < x * v + u * z + x * y.
rewrite the current goal using add_SNo_com(u * z)(x * y)LuzHxy (from left to right).
An exact proof term for the current goal is add_SNo_Lt2(x * v)(u * y + x * z)(x * y + u * z)HxvLuyxz(SNo_add_SNo(x * y)(u * z)HxyLuz)L1.
We will provex * v + u * z + x * y < x * y + u * v + x * z.
rewrite the current goal using add_SNo_rotate_3_1(x * v)(u * z)(x * y)HxvLuzHxy (from left to right).
We will provex * y + x * v + u * z < x * y + u * v + x * z.
An exact proof term for the current goal is add_SNo_Lt2(x * y)(x * v + u * z)(u * v + x * z)Hxy(SNo_add_SNo(x * v)(u * z)HxvLuz)LuvxzL2.
∀x y, SNox → SNoy → ∀u ∈ SNoL(x * y), ∀p : prop, (∀v ∈ SNoLx, ∀w ∈ SNoLy, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoRx, ∀w ∈ SNoRy, u + v * w ≤ v * y + x * w → p) → p
∀x y, SNox → SNoy → ∀u ∈ SNoR(x * y), ∀p : prop, (∀v ∈ SNoLx, ∀w ∈ SNoRy, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoRx, ∀w ∈ SNoLy, v * y + x * w ≤ u + v * w → p) → p
An exact proof term for the current goal is SNo_add_SNouyHu1Hy.
Applyadd_SNo_Lt1_cancel(v * z + x * w + y * w)(u * w)(x * z + y * z + v * w)LvzxwywLuwLxzyzvw to the current goal.
We will prove(v * z + x * w + y * w) + u * w < (x * z + y * z + v * w) + u * w.
rewrite the current goal using add_SNo_assoc_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw (from right to left).
rewrite the current goal using add_SNo_assoc_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw (from right to left).
We will provev * z + x * w + y * w + u * w < x * z + y * z + v * w + u * w.
ApplySNoLeLt_tra(v * z + x * w + y * w + u * w)(u * z + y * z + v * w + x * w)(x * z + y * z + v * w + u * w)(SNo_add_SNo_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw)(SNo_add_SNo_4(u * z)(y * z)(v * w)(x * w)LuzLyzLvwLxw)(SNo_add_SNo_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw) to the current goal.
We will provev * z + x * w + y * w + u * w ≤ u * z + y * z + v * w + x * w.
rewrite the current goal using add_SNo_com_3_0_1(v * z)(x * w)(y * w + u * w)LvzLxw(SNo_add_SNo(y * w)(u * w)LywLuw) (from left to right).
We will provex * w + v * z + y * w + u * w ≤ u * z + y * z + v * w + x * w.
rewrite the current goal using add_SNo_rotate_4_1(u * z)(y * z)(v * w)(x * w)LuzLyzLvwLxw (from left to right).
We will provex * w + v * z + y * w + u * w ≤ x * w + u * z + y * z + v * w.
Applyadd_SNo_Le2(x * w)(v * z + y * w + u * w)(u * z + y * z + v * w)Lxw(SNo_add_SNo_3(v * z)(y * w)(u * w)LvzLywLuw)(SNo_add_SNo_3(u * z)(y * z)(v * w)LuzLyzLvw) to the current goal.
We will provev * z + y * w + u * w ≤ u * z + y * z + v * w.
rewrite the current goal using add_SNo_com(y * w)(u * w)LywLuw (from left to right).
We will provev * z + u * w + y * w ≤ u * z + y * z + v * w.
rewrite the current goal using IHxzu(SNoL_SNoSxHxuHu)w(SNoL_SNoSzHzwHw) (from right to left).
We will provev * z + (u + y) * w ≤ u * z + y * z + v * w.
rewrite the current goal using add_SNo_assoc(u * z)(y * z)(v * w)LuzLyzLvw (from left to right).
We will provev * z + (u + y) * w ≤ (u * z + y * z) + v * w.
rewrite the current goal using IHxu(SNoL_SNoSxHxuHu) (from right to left).
We will provev * z + (u + y) * w ≤ (u + y) * z + v * w.
Applymul_SNo_Le(u + y)zvwLuyHzHv1Hw1 to the current goal.
We will proveu * z + y * z + v * w + x * w < x * z + y * z + v * w + u * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(y * z)(v * w + x * w)LuzLyz(SNo_add_SNo(v * w)(x * w)LvwLxw) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(x * z)(y * z)(v * w + u * w)LxzLyz(SNo_add_SNo(v * w)(u * w)LvwLuw) (from left to right).
We will provey * z + u * z + v * w + x * w < y * z + x * z + v * w + u * w.
Applyadd_SNo_Lt2(y * z)(u * z + v * w + x * w)(x * z + v * w + u * w)Lyz(SNo_add_SNo_3(u * z)(v * w)(x * w)LuzLvwLxw)(SNo_add_SNo_3(x * z)(v * w)(u * w)LxzLvwLuw) to the current goal.
We will proveu * z + v * w + x * w < x * z + v * w + u * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(v * w)(x * w)LuzLvwLxw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(x * z)(v * w)(u * w)LxzLvwLuw (from left to right).
We will provev * w + u * z + x * w < v * w + x * z + u * w.
Applyadd_SNo_Lt2(v * w)(u * z + x * w)(x * z + u * w)Lvw(SNo_add_SNo(u * z)(x * w)LuzLxw)(SNo_add_SNo(x * z)(u * w)LxzLuw) to the current goal.
We will proveu * z + x * w < x * z + u * w.
An exact proof term for the current goal is mul_SNo_LtxzuwHxHzHu1Hw1Hu3Hw3.
An exact proof term for the current goal is SNo_add_SNoxuHxHu1.
Applyadd_SNo_Lt1_cancel(v * z + x * w + y * w)(u * w)(x * z + y * z + v * w)LvzxwywLuwLxzyzvw to the current goal.
We will prove(v * z + x * w + y * w) + u * w < (x * z + y * z + v * w) + u * w.
rewrite the current goal using add_SNo_assoc_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw (from right to left).
rewrite the current goal using add_SNo_assoc_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw (from right to left).
We will provev * z + x * w + y * w + u * w < x * z + y * z + v * w + u * w.
ApplySNoLeLt_tra(v * z + x * w + y * w + u * w)(x * z + u * z + v * w + y * w)(x * z + y * z + v * w + u * w)(SNo_add_SNo_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw)(SNo_add_SNo_4(x * z)(u * z)(v * w)(y * w)LxzLuzLvwLyw)(SNo_add_SNo_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw) to the current goal.
We will provev * z + x * w + y * w + u * w ≤ x * z + u * z + v * w + y * w.
rewrite the current goal using add_SNo_com(y * w)(u * w)LywLuw (from left to right).
We will provev * z + x * w + u * w + y * w ≤ x * z + u * z + v * w + y * w.
rewrite the current goal using add_SNo_rotate_4_1(v * z)(x * w)(u * w)(y * w)LvzLxwLuwLyw (from left to right).
We will provey * w + v * z + x * w + u * w ≤ x * z + u * z + v * w + y * w.
rewrite the current goal using add_SNo_rotate_4_1(x * z)(u * z)(v * w)(y * w)LxzLuzLvwLyw (from left to right).
We will provey * w + v * z + x * w + u * w ≤ y * w + x * z + u * z + v * w.
Applyadd_SNo_Le2(y * w)(v * z + x * w + u * w)(x * z + u * z + v * w)Lyw(SNo_add_SNo_3(v * z)(x * w)(u * w)LvzLxwLuw)(SNo_add_SNo_3(x * z)(u * z)(v * w)LxzLuzLvw) to the current goal.
We will provev * z + x * w + u * w ≤ x * z + u * z + v * w.
rewrite the current goal using IHyzu(SNoL_SNoSyHyuHu)w(SNoL_SNoSzHzwHw) (from right to left).
We will provev * z + (x + u) * w ≤ x * z + u * z + v * w.
rewrite the current goal using add_SNo_assoc(x * z)(u * z)(v * w)LxzLuzLvw (from left to right).
We will provev * z + (x + u) * w ≤ (x * z + u * z) + v * w.
rewrite the current goal using IHyu(SNoL_SNoSyHyuHu) (from right to left).
We will provev * z + (x + u) * w ≤ (x + u) * z + v * w.
Applymul_SNo_Le(x + u)zvwLxuHzHv1Hw1 to the current goal.
We will provex * z + u * z + v * w + y * w < x * z + y * z + v * w + u * w.
Applyadd_SNo_Lt2(x * z)(u * z + v * w + y * w)(y * z + v * w + u * w)Lxz(SNo_add_SNo_3(u * z)(v * w)(y * w)LuzLvwLyw)(SNo_add_SNo_3(y * z)(v * w)(u * w)LyzLvwLuw) to the current goal.
We will proveu * z + v * w + y * w < y * z + v * w + u * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(v * w)(y * w)LuzLvwLyw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(y * z)(v * w)(u * w)LyzLvwLuw (from left to right).
We will provev * w + u * z + y * w < v * w + y * z + u * w.
Applyadd_SNo_Lt2(v * w)(u * z + y * w)(y * z + u * w)Lvw(SNo_add_SNo(u * z)(y * w)LuzLyw)(SNo_add_SNo(y * z)(u * w)LyzLuw) to the current goal.
We will proveu * z + y * w < y * z + u * w.
An exact proof term for the current goal is mul_SNo_LtyzuwHyHzHu1Hw1Hu3Hw3.
An exact proof term for the current goal is SNo_add_SNouyHu1Hy.
Applyadd_SNo_Lt1_cancel(v * z + x * w + y * w)(u * w)(x * z + y * z + v * w)LvzxwywLuwLxzyzvw to the current goal.
We will prove(v * z + x * w + y * w) + u * w < (x * z + y * z + v * w) + u * w.
rewrite the current goal using add_SNo_assoc_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw (from right to left).
rewrite the current goal using add_SNo_assoc_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw (from right to left).
We will provev * z + x * w + y * w + u * w < x * z + y * z + v * w + u * w.
ApplySNoLeLt_tra(v * z + x * w + y * w + u * w)(u * z + y * z + v * w + x * w)(x * z + y * z + v * w + u * w)(SNo_add_SNo_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw)(SNo_add_SNo_4(u * z)(y * z)(v * w)(x * w)LuzLyzLvwLxw)(SNo_add_SNo_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw) to the current goal.
We will provev * z + x * w + y * w + u * w ≤ u * z + y * z + v * w + x * w.
rewrite the current goal using add_SNo_com_3_0_1(v * z)(x * w)(y * w + u * w)LvzLxw(SNo_add_SNo(y * w)(u * w)LywLuw) (from left to right).
We will provex * w + v * z + y * w + u * w ≤ u * z + y * z + v * w + x * w.
rewrite the current goal using add_SNo_rotate_4_1(u * z)(y * z)(v * w)(x * w)LuzLyzLvwLxw (from left to right).
We will provex * w + v * z + y * w + u * w ≤ x * w + u * z + y * z + v * w.
Applyadd_SNo_Le2(x * w)(v * z + y * w + u * w)(u * z + y * z + v * w)Lxw(SNo_add_SNo_3(v * z)(y * w)(u * w)LvzLywLuw)(SNo_add_SNo_3(u * z)(y * z)(v * w)LuzLyzLvw) to the current goal.
We will provev * z + y * w + u * w ≤ u * z + y * z + v * w.
rewrite the current goal using add_SNo_com(y * w)(u * w)LywLuw (from left to right).
We will provev * z + u * w + y * w ≤ u * z + y * z + v * w.
rewrite the current goal using IHxzu(SNoR_SNoSxHxuHu)w(SNoR_SNoSzHzwHw) (from right to left).
We will provev * z + (u + y) * w ≤ u * z + y * z + v * w.
rewrite the current goal using add_SNo_assoc(u * z)(y * z)(v * w)LuzLyzLvw (from left to right).
We will provev * z + (u + y) * w ≤ (u * z + y * z) + v * w.
rewrite the current goal using IHxu(SNoR_SNoSxHxuHu) (from right to left).
We will provev * z + (u + y) * w ≤ (u + y) * z + v * w.
rewrite the current goal using add_SNo_com((u + y) * z)(v * w)(SNo_mul_SNo(u + y)zLuyHz)Lvw (from left to right).
rewrite the current goal using add_SNo_com(v * z)((u + y) * w)Lvz(SNo_mul_SNo(u + y)wLuyHw1) (from left to right).
Applymul_SNo_Levw(u + y)zHv1Hw1LuyHz to the current goal.
We will proveu * z + y * z + v * w + x * w < x * z + y * z + v * w + u * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(y * z)(v * w + x * w)LuzLyz(SNo_add_SNo(v * w)(x * w)LvwLxw) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(x * z)(y * z)(v * w + u * w)LxzLyz(SNo_add_SNo(v * w)(u * w)LvwLuw) (from left to right).
We will provey * z + u * z + v * w + x * w < y * z + x * z + v * w + u * w.
Applyadd_SNo_Lt2(y * z)(u * z + v * w + x * w)(x * z + v * w + u * w)Lyz(SNo_add_SNo_3(u * z)(v * w)(x * w)LuzLvwLxw)(SNo_add_SNo_3(x * z)(v * w)(u * w)LxzLvwLuw) to the current goal.
We will proveu * z + v * w + x * w < x * z + v * w + u * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(v * w)(x * w)LuzLvwLxw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(x * z)(v * w)(u * w)LxzLvwLuw (from left to right).
We will provev * w + u * z + x * w < v * w + x * z + u * w.
Applyadd_SNo_Lt2(v * w)(u * z + x * w)(x * z + u * w)Lvw(SNo_add_SNo(u * z)(x * w)LuzLxw)(SNo_add_SNo(x * z)(u * w)LxzLuw) to the current goal.
We will proveu * z + x * w < x * z + u * w.
rewrite the current goal using add_SNo_com(x * z)(u * w)LxzLuw (from left to right).
rewrite the current goal using add_SNo_com(u * z)(x * w)LuzLxw (from left to right).
We will provex * w + u * z < u * w + x * z.
An exact proof term for the current goal is mul_SNo_LtuwxzHu1Hw1HxHzHu3Hw3.
An exact proof term for the current goal is SNo_add_SNoxuHxHu1.
Applyadd_SNo_Lt1_cancel(v * z + x * w + y * w)(u * w)(x * z + y * z + v * w)LvzxwywLuwLxzyzvw to the current goal.
We will prove(v * z + x * w + y * w) + u * w < (x * z + y * z + v * w) + u * w.
rewrite the current goal using add_SNo_assoc_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw (from right to left).
rewrite the current goal using add_SNo_assoc_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw (from right to left).
We will provev * z + x * w + y * w + u * w < x * z + y * z + v * w + u * w.
ApplySNoLeLt_tra(v * z + x * w + y * w + u * w)(x * z + u * z + v * w + y * w)(x * z + y * z + v * w + u * w)(SNo_add_SNo_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw)(SNo_add_SNo_4(x * z)(u * z)(v * w)(y * w)LxzLuzLvwLyw)(SNo_add_SNo_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw) to the current goal.
We will provev * z + x * w + y * w + u * w ≤ x * z + u * z + v * w + y * w.
rewrite the current goal using add_SNo_com(y * w)(u * w)LywLuw (from left to right).
We will provev * z + x * w + u * w + y * w ≤ x * z + u * z + v * w + y * w.
rewrite the current goal using add_SNo_rotate_4_1(v * z)(x * w)(u * w)(y * w)LvzLxwLuwLyw (from left to right).
We will provey * w + v * z + x * w + u * w ≤ x * z + u * z + v * w + y * w.
rewrite the current goal using add_SNo_rotate_4_1(x * z)(u * z)(v * w)(y * w)LxzLuzLvwLyw (from left to right).
We will provey * w + v * z + x * w + u * w ≤ y * w + x * z + u * z + v * w.
Applyadd_SNo_Le2(y * w)(v * z + x * w + u * w)(x * z + u * z + v * w)Lyw(SNo_add_SNo_3(v * z)(x * w)(u * w)LvzLxwLuw)(SNo_add_SNo_3(x * z)(u * z)(v * w)LxzLuzLvw) to the current goal.
We will provev * z + x * w + u * w ≤ x * z + u * z + v * w.
rewrite the current goal using IHyzu(SNoR_SNoSyHyuHu)w(SNoR_SNoSzHzwHw) (from right to left).
We will provev * z + (x + u) * w ≤ x * z + u * z + v * w.
rewrite the current goal using add_SNo_assoc(x * z)(u * z)(v * w)LxzLuzLvw (from left to right).
We will provev * z + (x + u) * w ≤ (x * z + u * z) + v * w.
rewrite the current goal using IHyu(SNoR_SNoSyHyuHu) (from right to left).
We will provev * z + (x + u) * w ≤ (x + u) * z + v * w.
rewrite the current goal using add_SNo_com((x + u) * z)(v * w)(SNo_mul_SNo(x + u)zLxuHz)Lvw (from left to right).
rewrite the current goal using add_SNo_com(v * z)((x + u) * w)Lvz(SNo_mul_SNo(x + u)wLxuHw1) (from left to right).
Applymul_SNo_Levw(x + u)zHv1Hw1LxuHz to the current goal.
We will provex * z + u * z + v * w + y * w < x * z + y * z + v * w + u * w.
Applyadd_SNo_Lt2(x * z)(u * z + v * w + y * w)(y * z + v * w + u * w)Lxz(SNo_add_SNo_3(u * z)(v * w)(y * w)LuzLvwLyw)(SNo_add_SNo_3(y * z)(v * w)(u * w)LyzLvwLuw) to the current goal.
We will proveu * z + v * w + y * w < y * z + v * w + u * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(v * w)(y * w)LuzLvwLyw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(y * z)(v * w)(u * w)LyzLvwLuw (from left to right).
We will provev * w + u * z + y * w < v * w + y * z + u * w.
Applyadd_SNo_Lt2(v * w)(u * z + y * w)(y * z + u * w)Lvw(SNo_add_SNo(u * z)(y * w)LuzLyw)(SNo_add_SNo(y * z)(u * w)LyzLuw) to the current goal.
We will proveu * z + y * w < y * z + u * w.
rewrite the current goal using add_SNo_com(y * z)(u * w)LyzLuw (from left to right).
rewrite the current goal using add_SNo_com(u * z)(y * w)LuzLyw (from left to right).
We will provey * w + u * z < u * w + y * z.
An exact proof term for the current goal is mul_SNo_LtuwyzHu1Hw1HyHzHu3Hw3.
Letu be given.
AssumeHu: u ∈ R.
rewrite the current goal using LE (from right to left).
An exact proof term for the current goal is SNo_add_SNouyHu1Hy.
Applyadd_SNo_Lt1_cancel(x * z + y * z + v * w)(u * w)(v * z + x * w + y * w)LxzyzvwLuwLvzxwyw to the current goal.
We will prove(x * z + y * z + v * w) + u * w < (v * z + x * w + y * w) + u * w.
rewrite the current goal using add_SNo_assoc_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw (from right to left).
rewrite the current goal using add_SNo_assoc_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw (from right to left).
We will provex * z + y * z + v * w + u * w < v * z + x * w + y * w + u * w.
ApplySNoLtLe_tra(x * z + y * z + v * w + u * w)(u * z + y * z + v * w + x * w)(v * z + x * w + y * w + u * w)(SNo_add_SNo_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw)(SNo_add_SNo_4(u * z)(y * z)(v * w)(x * w)LuzLyzLvwLxw)(SNo_add_SNo_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw) to the current goal.
We will provex * z + y * z + v * w + u * w < u * z + y * z + v * w + x * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(y * z)(v * w + x * w)LuzLyz(SNo_add_SNo(v * w)(x * w)LvwLxw) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(x * z)(y * z)(v * w + u * w)LxzLyz(SNo_add_SNo(v * w)(u * w)LvwLuw) (from left to right).
We will provey * z + x * z + v * w + u * w < y * z + u * z + v * w + x * w.
Applyadd_SNo_Lt2(y * z)(x * z + v * w + u * w)(u * z + v * w + x * w)Lyz(SNo_add_SNo_3(x * z)(v * w)(u * w)LxzLvwLuw)(SNo_add_SNo_3(u * z)(v * w)(x * w)LuzLvwLxw) to the current goal.
We will provex * z + v * w + u * w < u * z + v * w + x * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(v * w)(x * w)LuzLvwLxw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(x * z)(v * w)(u * w)LxzLvwLuw (from left to right).
We will provev * w + x * z + u * w < v * w + u * z + x * w.
Applyadd_SNo_Lt2(v * w)(x * z + u * w)(u * z + x * w)Lvw(SNo_add_SNo(x * z)(u * w)LxzLuw)(SNo_add_SNo(u * z)(x * w)LuzLxw) to the current goal.
We will provex * z + u * w < u * z + x * w.
rewrite the current goal using add_SNo_com(x * z)(u * w)LxzLuw (from left to right).
rewrite the current goal using add_SNo_com(u * z)(x * w)LuzLxw (from left to right).
An exact proof term for the current goal is mul_SNo_LtxwuzHxHw1Hu1HzHu3Hw3.
We will proveu * z + y * z + v * w + x * w ≤ v * z + x * w + y * w + u * w.
rewrite the current goal using add_SNo_com_3_0_1(v * z)(x * w)(y * w + u * w)LvzLxw(SNo_add_SNo(y * w)(u * w)LywLuw) (from left to right).
We will proveu * z + y * z + v * w + x * w ≤ x * w + v * z + y * w + u * w.
rewrite the current goal using add_SNo_rotate_4_1(u * z)(y * z)(v * w)(x * w)LuzLyzLvwLxw (from left to right).
We will provex * w + u * z + y * z + v * w ≤ x * w + v * z + y * w + u * w.
Applyadd_SNo_Le2(x * w)(u * z + y * z + v * w)(v * z + y * w + u * w)Lxw(SNo_add_SNo_3(u * z)(y * z)(v * w)LuzLyzLvw)(SNo_add_SNo_3(v * z)(y * w)(u * w)LvzLywLuw) to the current goal.
We will proveu * z + y * z + v * w ≤ v * z + y * w + u * w.
rewrite the current goal using add_SNo_com(y * w)(u * w)LywLuw (from left to right).
We will proveu * z + y * z + v * w ≤ v * z + u * w + y * w.
rewrite the current goal using IHxzu(SNoL_SNoSxHxuHu)w(SNoR_SNoSzHzwHw) (from right to left).
We will proveu * z + y * z + v * w ≤ v * z + (u + y) * w.
rewrite the current goal using add_SNo_assoc(u * z)(y * z)(v * w)LuzLyzLvw (from left to right).
We will prove(u * z + y * z) + v * w ≤ v * z + (u + y) * w.
rewrite the current goal using IHxu(SNoL_SNoSxHxuHu) (from right to left).
We will prove(u + y) * z + v * w ≤ v * z + (u + y) * w.
rewrite the current goal using add_SNo_com((u + y) * z)(v * w)(SNo_mul_SNo(u + y)zLuyHz)Lvw (from left to right).
rewrite the current goal using add_SNo_com(v * z)((u + y) * w)Lvz(SNo_mul_SNo(u + y)wLuyHw1) (from left to right).
We will provev * w + (u + y) * z ≤ (u + y) * w + v * z.
Applymul_SNo_Le(u + y)wvzLuyHw1Hv1Hz to the current goal.
An exact proof term for the current goal is SNo_add_SNoxuHxHu1.
Applyadd_SNo_Lt1_cancel(x * z + y * z + v * w)(u * w)(v * z + x * w + y * w)LxzyzvwLuwLvzxwyw to the current goal.
We will prove(x * z + y * z + v * w) + u * w < (v * z + x * w + y * w) + u * w.
rewrite the current goal using add_SNo_assoc_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw (from right to left).
rewrite the current goal using add_SNo_assoc_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw (from right to left).
We will provex * z + y * z + v * w + u * w < v * z + x * w + y * w + u * w.
ApplySNoLtLe_tra(x * z + y * z + v * w + u * w)(x * z + u * z + v * w + y * w)(v * z + x * w + y * w + u * w)(SNo_add_SNo_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw)(SNo_add_SNo_4(x * z)(u * z)(v * w)(y * w)LxzLuzLvwLyw)(SNo_add_SNo_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw) to the current goal.
We will provex * z + y * z + v * w + u * w < x * z + u * z + v * w + y * w.
Applyadd_SNo_Lt2(x * z)(y * z + v * w + u * w)(u * z + v * w + y * w)Lxz(SNo_add_SNo_3(y * z)(v * w)(u * w)LyzLvwLuw)(SNo_add_SNo_3(u * z)(v * w)(y * w)LuzLvwLyw) to the current goal.
We will provey * z + v * w + u * w < u * z + v * w + y * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(v * w)(y * w)LuzLvwLyw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(y * z)(v * w)(u * w)LyzLvwLuw (from left to right).
We will provev * w + y * z + u * w < v * w + u * z + y * w.
Applyadd_SNo_Lt2(v * w)(y * z + u * w)(u * z + y * w)Lvw(SNo_add_SNo(y * z)(u * w)LyzLuw)(SNo_add_SNo(u * z)(y * w)LuzLyw) to the current goal.
We will provey * z + u * w < u * z + y * w.
rewrite the current goal using add_SNo_com(y * z)(u * w)LyzLuw (from left to right).
rewrite the current goal using add_SNo_com(u * z)(y * w)LuzLyw (from left to right).
An exact proof term for the current goal is mul_SNo_LtywuzHyHw1Hu1HzHu3Hw3.
We will provex * z + u * z + v * w + y * w ≤ v * z + x * w + y * w + u * w.
rewrite the current goal using add_SNo_com(y * w)(u * w)LywLuw (from left to right).
We will provex * z + u * z + v * w + y * w ≤ v * z + x * w + u * w + y * w.
rewrite the current goal using add_SNo_rotate_4_1(v * z)(x * w)(u * w)(y * w)LvzLxwLuwLyw (from left to right).
We will provex * z + u * z + v * w + y * w ≤ y * w + v * z + x * w + u * w.
rewrite the current goal using add_SNo_rotate_4_1(x * z)(u * z)(v * w)(y * w)LxzLuzLvwLyw (from left to right).
We will provey * w + x * z + u * z + v * w ≤ y * w + v * z + x * w + u * w.
Applyadd_SNo_Le2(y * w)(x * z + u * z + v * w)(v * z + x * w + u * w)Lyw(SNo_add_SNo_3(x * z)(u * z)(v * w)LxzLuzLvw)(SNo_add_SNo_3(v * z)(x * w)(u * w)LvzLxwLuw) to the current goal.
We will provex * z + u * z + v * w ≤ v * z + x * w + u * w.
rewrite the current goal using IHyzu(SNoL_SNoSyHyuHu)w(SNoR_SNoSzHzwHw) (from right to left).
We will provex * z + u * z + v * w ≤ v * z + (x + u) * w.
rewrite the current goal using add_SNo_assoc(x * z)(u * z)(v * w)LxzLuzLvw (from left to right).
We will prove(x * z + u * z) + v * w ≤ v * z + (x + u) * w.
rewrite the current goal using IHyu(SNoL_SNoSyHyuHu) (from right to left).
We will prove(x + u) * z + v * w ≤ v * z + (x + u) * w.
rewrite the current goal using add_SNo_com((x + u) * z)(v * w)(SNo_mul_SNo(x + u)zLxuHz)Lvw (from left to right).
rewrite the current goal using add_SNo_com(v * z)((x + u) * w)Lvz(SNo_mul_SNo(x + u)wLxuHw1) (from left to right).
We will provev * w + (x + u) * z ≤ (x + u) * w + v * z.
Applymul_SNo_Le(x + u)wvzLxuHw1Hv1Hz to the current goal.
An exact proof term for the current goal is SNo_add_SNouyHu1Hy.
Applyadd_SNo_Lt1_cancel(x * z + y * z + v * w)(u * w)(v * z + x * w + y * w)LxzyzvwLuwLvzxwyw to the current goal.
We will prove(x * z + y * z + v * w) + u * w < (v * z + x * w + y * w) + u * w.
rewrite the current goal using add_SNo_assoc_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw (from right to left).
rewrite the current goal using add_SNo_assoc_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw (from right to left).
We will provex * z + y * z + v * w + u * w < v * z + x * w + y * w + u * w.
ApplySNoLtLe_tra(x * z + y * z + v * w + u * w)(u * z + y * z + v * w + x * w)(v * z + x * w + y * w + u * w)(SNo_add_SNo_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw)(SNo_add_SNo_4(u * z)(y * z)(v * w)(x * w)LuzLyzLvwLxw)(SNo_add_SNo_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw) to the current goal.
We will provex * z + y * z + v * w + u * w < u * z + y * z + v * w + x * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(y * z)(v * w + x * w)LuzLyz(SNo_add_SNo(v * w)(x * w)LvwLxw) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(x * z)(y * z)(v * w + u * w)LxzLyz(SNo_add_SNo(v * w)(u * w)LvwLuw) (from left to right).
We will provey * z + x * z + v * w + u * w < y * z + u * z + v * w + x * w.
Applyadd_SNo_Lt2(y * z)(x * z + v * w + u * w)(u * z + v * w + x * w)Lyz(SNo_add_SNo_3(x * z)(v * w)(u * w)LxzLvwLuw)(SNo_add_SNo_3(u * z)(v * w)(x * w)LuzLvwLxw) to the current goal.
We will provex * z + v * w + u * w < u * z + v * w + x * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(v * w)(x * w)LuzLvwLxw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(x * z)(v * w)(u * w)LxzLvwLuw (from left to right).
We will provev * w + x * z + u * w < v * w + u * z + x * w.
Applyadd_SNo_Lt2(v * w)(x * z + u * w)(u * z + x * w)Lvw(SNo_add_SNo(x * z)(u * w)LxzLuw)(SNo_add_SNo(u * z)(x * w)LuzLxw) to the current goal.
We will provex * z + u * w < u * z + x * w.
An exact proof term for the current goal is mul_SNo_LtuzxwHu1HzHxHw1Hu3Hw3.
We will proveu * z + y * z + v * w + x * w ≤ v * z + x * w + y * w + u * w.
rewrite the current goal using add_SNo_com_3_0_1(v * z)(x * w)(y * w + u * w)LvzLxw(SNo_add_SNo(y * w)(u * w)LywLuw) (from left to right).
We will proveu * z + y * z + v * w + x * w ≤ x * w + v * z + y * w + u * w.
rewrite the current goal using add_SNo_rotate_4_1(u * z)(y * z)(v * w)(x * w)LuzLyzLvwLxw (from left to right).
We will provex * w + u * z + y * z + v * w ≤ x * w + v * z + y * w + u * w.
Applyadd_SNo_Le2(x * w)(u * z + y * z + v * w)(v * z + y * w + u * w)Lxw(SNo_add_SNo_3(u * z)(y * z)(v * w)LuzLyzLvw)(SNo_add_SNo_3(v * z)(y * w)(u * w)LvzLywLuw) to the current goal.
We will proveu * z + y * z + v * w ≤ v * z + y * w + u * w.
rewrite the current goal using add_SNo_com(y * w)(u * w)LywLuw (from left to right).
We will proveu * z + y * z + v * w ≤ v * z + u * w + y * w.
rewrite the current goal using IHxzu(SNoR_SNoSxHxuHu)w(SNoL_SNoSzHzwHw) (from right to left).
We will proveu * z + y * z + v * w ≤ v * z + (u + y) * w.
rewrite the current goal using add_SNo_assoc(u * z)(y * z)(v * w)LuzLyzLvw (from left to right).
We will prove(u * z + y * z) + v * w ≤ v * z + (u + y) * w.
rewrite the current goal using IHxu(SNoR_SNoSxHxuHu) (from right to left).
We will prove(u + y) * z + v * w ≤ v * z + (u + y) * w.
Applymul_SNo_Levz(u + y)wHv1HzLuyHw1 to the current goal.
An exact proof term for the current goal is SNo_add_SNoxuHxHu1.
Applyadd_SNo_Lt1_cancel(x * z + y * z + v * w)(u * w)(v * z + x * w + y * w)LxzyzvwLuwLvzxwyw to the current goal.
We will prove(x * z + y * z + v * w) + u * w < (v * z + x * w + y * w) + u * w.
rewrite the current goal using add_SNo_assoc_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw (from right to left).
rewrite the current goal using add_SNo_assoc_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw (from right to left).
We will provex * z + y * z + v * w + u * w < v * z + x * w + y * w + u * w.
ApplySNoLtLe_tra(x * z + y * z + v * w + u * w)(x * z + u * z + v * w + y * w)(v * z + x * w + y * w + u * w)(SNo_add_SNo_4(x * z)(y * z)(v * w)(u * w)LxzLyzLvwLuw)(SNo_add_SNo_4(x * z)(u * z)(v * w)(y * w)LxzLuzLvwLyw)(SNo_add_SNo_4(v * z)(x * w)(y * w)(u * w)LvzLxwLywLuw) to the current goal.
We will provex * z + y * z + v * w + u * w < x * z + u * z + v * w + y * w.
Applyadd_SNo_Lt2(x * z)(y * z + v * w + u * w)(u * z + v * w + y * w)Lxz(SNo_add_SNo_3(y * z)(v * w)(u * w)LyzLvwLuw)(SNo_add_SNo_3(u * z)(v * w)(y * w)LuzLvwLyw) to the current goal.
We will provey * z + v * w + u * w < u * z + v * w + y * w.
rewrite the current goal using add_SNo_com_3_0_1(u * z)(v * w)(y * w)LuzLvwLyw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1(y * z)(v * w)(u * w)LyzLvwLuw (from left to right).
We will provev * w + y * z + u * w < v * w + u * z + y * w.
Applyadd_SNo_Lt2(v * w)(y * z + u * w)(u * z + y * w)Lvw(SNo_add_SNo(y * z)(u * w)LyzLuw)(SNo_add_SNo(u * z)(y * w)LuzLyw) to the current goal.
We will provey * z + u * w < u * z + y * w.
An exact proof term for the current goal is mul_SNo_LtuzywHu1HzHyHw1Hu3Hw3.
We will provex * z + u * z + v * w + y * w ≤ v * z + x * w + y * w + u * w.
rewrite the current goal using add_SNo_com(y * w)(u * w)LywLuw (from left to right).
We will provex * z + u * z + v * w + y * w ≤ v * z + x * w + u * w + y * w.
rewrite the current goal using add_SNo_rotate_4_1(v * z)(x * w)(u * w)(y * w)LvzLxwLuwLyw (from left to right).
We will provex * z + u * z + v * w + y * w ≤ y * w + v * z + x * w + u * w.
rewrite the current goal using add_SNo_rotate_4_1(x * z)(u * z)(v * w)(y * w)LxzLuzLvwLyw (from left to right).
We will provey * w + x * z + u * z + v * w ≤ y * w + v * z + x * w + u * w.
Applyadd_SNo_Le2(y * w)(x * z + u * z + v * w)(v * z + x * w + u * w)Lyw(SNo_add_SNo_3(x * z)(u * z)(v * w)LxzLuzLvw)(SNo_add_SNo_3(v * z)(x * w)(u * w)LvzLxwLuw) to the current goal.
We will provex * z + u * z + v * w ≤ v * z + x * w + u * w.
rewrite the current goal using IHyzu(SNoR_SNoSyHyuHu)w(SNoL_SNoSzHzwHw) (from right to left).
We will provex * z + u * z + v * w ≤ v * z + (x + u) * w.
rewrite the current goal using add_SNo_assoc(x * z)(u * z)(v * w)LxzLuzLvw (from left to right).
We will prove(x * z + u * z) + v * w ≤ v * z + (x + u) * w.
rewrite the current goal using IHyu(SNoR_SNoSyHyuHu) (from right to left).
We will prove(x + u) * z + v * w ≤ v * z + (x + u) * w.
Applymul_SNo_Levz(x + u)wHv1HzLxuHw1 to the current goal.
An exact proof term for the current goal is SNo_mul_SNoywHyHw1.
We prove the intermediate claimLuyz: SNo(u + y * z).
An exact proof term for the current goal is SNo_add_SNou(y * z)Hu1Lyz.
We prove the intermediate claimLvwyw: SNo(v * w + y * w).
An exact proof term for the current goal is SNo_add_SNo(v * w)(y * w)LvwLyw.
We prove the intermediate claimLvzxw: SNo(v * z + x * w).
An exact proof term for the current goal is SNo_add_SNo(v * z)(x * w)LvzLxw.
We will proveu + y * z < (x + y) * z.
Applyadd_SNo_Lt1_cancel(u + y * z)(v * w + y * w)((x + y) * z)LuyzLvwywLxyz to the current goal.
We will prove(u + y * z) + v * w + y * w < (x + y) * z + v * w + y * w.
rewrite the current goal using add_SNo_com_4_inner_midu(y * z)(v * w)(y * w)Hu1LyzLvwLyw (from left to right).
We will prove(u + v * w) + y * z + y * w < (x + y) * z + v * w + y * w.
ApplySNoLeLt_tra((u + v * w) + y * z + y * w)(v * z + y * z + x * w + y * w)((x + y) * z + v * w + y * w)(SNo_add_SNo_3(u + v * w)(y * z)(y * w)LuvwLyzLyw)(SNo_add_SNo_4(v * z)(y * z)(x * w)(y * w)LvzLyzLxwLyw)(SNo_add_SNo_3((x + y) * z)(v * w)(y * w)LxyzLvwLyw) to the current goal.
We will prove(u + v * w) + y * z + y * w ≤ v * z + y * z + x * w + y * w.
rewrite the current goal using add_SNo_assoc(v * z)(y * z)(x * w + y * w)LvzLyz(SNo_add_SNo(x * w)(y * w)LxwLyw) (from left to right).
We will prove(u + v * w) + y * z + y * w ≤ (v * z + y * z) + x * w + y * w.
rewrite the current goal using add_SNo_com_4_inner_mid(v * z)(y * z)(x * w)(y * w)LvzLyzLxwLyw (from left to right).
We will prove(u + v * w) + y * z + y * w ≤ (v * z + x * w) + y * z + y * w.
Applyadd_SNo_Le1(u + v * w)(y * z + y * w)(v * z + x * w)Luvw(SNo_add_SNo(y * z)(y * w)LyzLyw)(SNo_add_SNo(v * z)(x * w)LvzLxw) to the current goal.
We will proveu + v * w ≤ v * z + x * w.
An exact proof term for the current goal is Hvw.
We will provev * z + y * z + x * w + y * w < (x + y) * z + v * w + y * w.
rewrite the current goal using IHzw(SNoL_SNoSzHzwHw) (from right to left).
We will provev * z + y * z + (x + y) * w < (x + y) * z + v * w + y * w.
rewrite the current goal using IHxzv(SNoL_SNoSxHxvHv)w(SNoL_SNoSzHzwHw) (from right to left).
We will provev * z + y * z + (x + y) * w < (x + y) * z + (v + y) * w.
rewrite the current goal using add_SNo_assoc(v * z)(y * z)((x + y) * w)LvzLyzLxyw (from left to right).
rewrite the current goal using IHxv(SNoL_SNoSxHxvHv) (from right to left).
We will prove(v + y) * z + (x + y) * w < (x + y) * z + (v + y) * w.
Applymul_SNo_Lt(x + y)z(v + y)wLxyHzLvyHw1 to the current goal.
An exact proof term for the current goal is SNo_mul_SNoywHyHw1.
We prove the intermediate claimLuyz: SNo(u + y * z).
An exact proof term for the current goal is SNo_add_SNou(y * z)Hu1Lyz.
We prove the intermediate claimLvwyw: SNo(v * w + y * w).
An exact proof term for the current goal is SNo_add_SNo(v * w)(y * w)LvwLyw.
We will proveu + y * z < (x + y) * z.
Applyadd_SNo_Lt1_cancel(u + y * z)(v * w + y * w)((x + y) * z)LuyzLvwywLxyz to the current goal.
We will prove(u + y * z) + v * w + y * w < (x + y) * z + v * w + y * w.
rewrite the current goal using add_SNo_com_4_inner_midu(y * z)(v * w)(y * w)Hu1LyzLvwLyw (from left to right).
We will prove(u + v * w) + y * z + y * w < (x + y) * z + v * w + y * w.
ApplySNoLeLt_tra((u + v * w) + y * z + y * w)(v * z + y * z + x * w + y * w)((x + y) * z + v * w + y * w)(SNo_add_SNo_3(u + v * w)(y * z)(y * w)LuvwLyzLyw)(SNo_add_SNo_4(v * z)(y * z)(x * w)(y * w)LvzLyzLxwLyw)(SNo_add_SNo_3((x + y) * z)(v * w)(y * w)LxyzLvwLyw) to the current goal.
We will prove(u + v * w) + y * z + y * w ≤ v * z + y * z + x * w + y * w.
rewrite the current goal using add_SNo_assoc(v * z)(y * z)(x * w + y * w)LvzLyz(SNo_add_SNo(x * w)(y * w)LxwLyw) (from left to right).
We will prove(u + v * w) + y * z + y * w ≤ (v * z + y * z) + x * w + y * w.
rewrite the current goal using add_SNo_com_4_inner_mid(v * z)(y * z)(x * w)(y * w)LvzLyzLxwLyw (from left to right).
We will prove(u + v * w) + y * z + y * w ≤ (v * z + x * w) + y * z + y * w.
Applyadd_SNo_Le1(u + v * w)(y * z + y * w)(v * z + x * w)Luvw(SNo_add_SNo(y * z)(y * w)LyzLyw)(SNo_add_SNo(v * z)(x * w)LvzLxw) to the current goal.
We will proveu + v * w ≤ v * z + x * w.
An exact proof term for the current goal is Hvw.
We will provev * z + y * z + x * w + y * w < (x + y) * z + v * w + y * w.
rewrite the current goal using IHzw(SNoR_SNoSzHzwHw) (from right to left).
We will provev * z + y * z + (x + y) * w < (x + y) * z + v * w + y * w.
rewrite the current goal using IHxzv(SNoR_SNoSxHxvHv)w(SNoR_SNoSzHzwHw) (from right to left).
We will provev * z + y * z + (x + y) * w < (x + y) * z + (v + y) * w.
rewrite the current goal using add_SNo_assoc(v * z)(y * z)((x + y) * w)LvzLyzLxyw (from left to right).
rewrite the current goal using IHxv(SNoR_SNoSxHxvHv) (from right to left).
We will prove(v + y) * z + (x + y) * w < (x + y) * z + (v + y) * w.
rewrite the current goal using add_SNo_com((v + y) * z)((x + y) * w)(SNo_mul_SNo(v + y)zLvyHz)Lxyw (from left to right).
rewrite the current goal using add_SNo_com((x + y) * z)((v + y) * w)Lxyz(SNo_mul_SNo(v + y)wLvyHw1) (from left to right).
Applymul_SNo_Lt(v + y)w(x + y)zLvyHw1LxyHz to the current goal.
An exact proof term for the current goal is SNo_mul_SNoywHyHw1.
We prove the intermediate claimLuxz: SNo(u + x * z).
An exact proof term for the current goal is SNo_add_SNou(x * z)Hu1Lxz.
We prove the intermediate claimLvwxw: SNo(v * w + x * w).
An exact proof term for the current goal is SNo_add_SNo(v * w)(x * w)LvwLxw.
We will proveu + x * z < (x + y) * z.
Applyadd_SNo_Lt1_cancel(u + x * z)(v * w + x * w)((x + y) * z)LuxzLvwxwLxyz to the current goal.
We will prove(u + x * z) + v * w + x * w < (x + y) * z + v * w + x * w.
rewrite the current goal using add_SNo_com_4_inner_midu(x * z)(v * w)(x * w)Hu1LxzLvwLxw (from left to right).
We will prove(u + v * w) + x * z + x * w < (x + y) * z + v * w + x * w.
ApplySNoLeLt_tra((u + v * w) + x * z + x * w)(v * z + x * z + x * w + y * w)((x + y) * z + v * w + x * w)(SNo_add_SNo_3(u + v * w)(x * z)(x * w)LuvwLxzLxw)(SNo_add_SNo_4(v * z)(x * z)(x * w)(y * w)LvzLxzLxwLyw)(SNo_add_SNo_3((x + y) * z)(v * w)(x * w)LxyzLvwLxw) to the current goal.
We will prove(u + v * w) + x * z + x * w ≤ v * z + x * z + x * w + y * w.
rewrite the current goal using add_SNo_assoc(v * z)(x * z)(x * w + y * w)LvzLxz(SNo_add_SNo(x * w)(y * w)LxwLyw) (from left to right).
We will prove(u + v * w) + x * z + x * w ≤ (v * z + x * z) + x * w + y * w.
rewrite the current goal using add_SNo_com(x * w)(y * w)LxwLyw (from left to right).
We will prove(u + v * w) + x * z + x * w ≤ (v * z + x * z) + y * w + x * w.
rewrite the current goal using add_SNo_com_4_inner_mid(v * z)(x * z)(y * w)(x * w)LvzLxzLywLxw (from left to right).
We will prove(u + v * w) + x * z + x * w ≤ (v * z + y * w) + x * z + x * w.
Applyadd_SNo_Le1(u + v * w)(x * z + x * w)(v * z + y * w)Luvw(SNo_add_SNo(x * z)(x * w)LxzLxw)(SNo_add_SNo(v * z)(y * w)LvzLyw) to the current goal.
We will proveu + v * w ≤ v * z + y * w.
An exact proof term for the current goal is Hvw.
We will provev * z + x * z + x * w + y * w < (x + y) * z + v * w + x * w.
rewrite the current goal using IHzw(SNoL_SNoSzHzwHw) (from right to left).
We will provev * z + x * z + (x + y) * w < (x + y) * z + v * w + x * w.
rewrite the current goal using add_SNo_com(v * w)(x * w)LvwLxw (from left to right).
rewrite the current goal using IHyzv(SNoL_SNoSyHyvHv)w(SNoL_SNoSzHzwHw) (from right to left).
We will provev * z + x * z + (x + y) * w < (x + y) * z + (x + v) * w.
rewrite the current goal using add_SNo_assoc(v * z)(x * z)((x + y) * w)LvzLxzLxyw (from left to right).
We will prove(v * z + x * z) + (x + y) * w < (x + y) * z + (x + v) * w.
rewrite the current goal using add_SNo_com(v * z)(x * z)LvzLxz (from left to right).
We will prove(x * z + v * z) + (x + y) * w < (x + y) * z + (x + v) * w.
rewrite the current goal using IHyv(SNoL_SNoSyHyvHv) (from right to left).
We will prove(x + v) * z + (x + y) * w < (x + y) * z + (x + v) * w.
Applymul_SNo_Lt(x + y)z(x + v)wLxyHzLxvHw1 to the current goal.
An exact proof term for the current goal is SNo_mul_SNoywHyHw1.
We prove the intermediate claimLuxz: SNo(u + x * z).
An exact proof term for the current goal is SNo_add_SNou(x * z)Hu1Lxz.
We prove the intermediate claimLvwxw: SNo(v * w + x * w).
An exact proof term for the current goal is SNo_add_SNo(v * w)(x * w)LvwLxw.
We prove the intermediate claimLvzxw: SNo(v * z + x * w).
An exact proof term for the current goal is SNo_add_SNo(v * z)(x * w)LvzLxw.
We will proveu + x * z < (x + y) * z.
Applyadd_SNo_Lt1_cancel(u + x * z)(v * w + x * w)((x + y) * z)LuxzLvwxwLxyz to the current goal.
We will prove(u + x * z) + v * w + x * w < (x + y) * z + v * w + x * w.
rewrite the current goal using add_SNo_com_4_inner_midu(x * z)(v * w)(x * w)Hu1LxzLvwLxw (from left to right).
We will prove(u + v * w) + x * z + x * w < (x + y) * z + v * w + x * w.
ApplySNoLeLt_tra((u + v * w) + x * z + x * w)(v * z + x * z + x * w + y * w)((x + y) * z + v * w + x * w)(SNo_add_SNo_3(u + v * w)(x * z)(x * w)LuvwLxzLxw)(SNo_add_SNo_4(v * z)(x * z)(x * w)(y * w)LvzLxzLxwLyw)(SNo_add_SNo_3((x + y) * z)(v * w)(x * w)LxyzLvwLxw) to the current goal.
We will prove(u + v * w) + x * z + x * w ≤ v * z + x * z + x * w + y * w.
rewrite the current goal using add_SNo_assoc(v * z)(x * z)(x * w + y * w)LvzLxz(SNo_add_SNo(x * w)(y * w)LxwLyw) (from left to right).
rewrite the current goal using add_SNo_com(y * w)(x * w)LywLxw (from right to left).
We will prove(u + v * w) + x * z + x * w ≤ (v * z + x * z) + y * w + x * w.
rewrite the current goal using add_SNo_com_4_inner_mid(v * z)(x * z)(y * w)(x * w)LvzLxzLywLxw (from left to right).
We will prove(u + v * w) + x * z + x * w ≤ (v * z + y * w) + x * z + x * w.
Applyadd_SNo_Le1(u + v * w)(x * z + x * w)(v * z + y * w)Luvw(SNo_add_SNo(x * z)(x * w)LxzLxw)(SNo_add_SNo(v * z)(y * w)LvzLyw) to the current goal.
We will proveu + v * w ≤ v * z + y * w.
An exact proof term for the current goal is Hvw.
We will provev * z + x * z + x * w + y * w < (x + y) * z + v * w + x * w.
rewrite the current goal using IHzw(SNoR_SNoSzHzwHw) (from right to left).
We will provev * z + x * z + (x + y) * w < (x + y) * z + v * w + x * w.
rewrite the current goal using add_SNo_com(v * w)(x * w)LvwLxw (from left to right).
We will provev * z + x * z + (x + y) * w < (x + y) * z + x * w + v * w.
rewrite the current goal using IHyzv(SNoR_SNoSyHyvHv)w(SNoR_SNoSzHzwHw) (from right to left).
We will provev * z + x * z + (x + y) * w < (x + y) * z + (x + v) * w.
rewrite the current goal using add_SNo_assoc(v * z)(x * z)((x + y) * w)LvzLxzLxyw (from left to right).
We will prove(v * z + x * z) + (x + y) * w < (x + y) * z + (x + v) * w.
rewrite the current goal using add_SNo_com(v * z)(x * z)LvzLxz (from left to right).
rewrite the current goal using IHyv(SNoR_SNoSyHyvHv) (from right to left).
We will prove(x + v) * z + (x + y) * w < (x + y) * z + (x + v) * w.
rewrite the current goal using add_SNo_com((x + v) * z)((x + y) * w)(SNo_mul_SNo(x + v)zLxvHz)Lxyw (from left to right).
rewrite the current goal using add_SNo_com((x + y) * z)((x + v) * w)Lxyz(SNo_mul_SNo(x + v)wLxvHw1) (from left to right).
We will prove(x + y) * w + (x + v) * z < (x + v) * w + (x + y) * z.
Applymul_SNo_Lt(x + v)w(x + y)zLxvHw1LxyHz to the current goal.
An exact proof term for the current goal is SNo_mul_SNoywHyHw1.
We prove the intermediate claimLuyz: SNo(u + y * z).
An exact proof term for the current goal is SNo_add_SNou(y * z)Hu1Lyz.
We prove the intermediate claimLvwyw: SNo(v * w + y * w).
An exact proof term for the current goal is SNo_add_SNo(v * w)(y * w)LvwLyw.
We prove the intermediate claimLvzxw: SNo(v * z + x * w).
An exact proof term for the current goal is SNo_add_SNo(v * z)(x * w)LvzLxw.
We will prove(x + y) * z < u + y * z.
Applyadd_SNo_Lt1_cancel((x + y) * z)(v * w + y * w)(u + y * z)LxyzLvwywLuyz to the current goal.
We will prove(x + y) * z + v * w + y * w < (u + y * z) + v * w + y * w.
rewrite the current goal using add_SNo_com_4_inner_midu(y * z)(v * w)(y * w)Hu1LyzLvwLyw (from left to right).
We will prove(x + y) * z + v * w + y * w < (u + v * w) + y * z + y * w.
ApplySNoLtLe_tra((x + y) * z + v * w + y * w)(v * z + y * z + x * w + y * w)((u + v * w) + y * z + y * w)(SNo_add_SNo_3((x + y) * z)(v * w)(y * w)LxyzLvwLyw)(SNo_add_SNo_4(v * z)(y * z)(x * w)(y * w)LvzLyzLxwLyw)(SNo_add_SNo_3(u + v * w)(y * z)(y * w)LuvwLyzLyw) to the current goal.
We will prove(x + y) * z + v * w + y * w < v * z + y * z + x * w + y * w.
rewrite the current goal using IHzw(SNoR_SNoSzHzwHw) (from right to left).
We will prove(x + y) * z + v * w + y * w < v * z + y * z + (x + y) * w.
rewrite the current goal using IHxzv(SNoL_SNoSxHxvHv)w(SNoR_SNoSzHzwHw) (from right to left).
We will prove(x + y) * z + (v + y) * w < v * z + y * z + (x + y) * w.
rewrite the current goal using add_SNo_assoc(v * z)(y * z)((x + y) * w)LvzLyzLxyw (from left to right).
rewrite the current goal using IHxv(SNoL_SNoSxHxvHv) (from right to left).
We will prove(x + y) * z + (v + y) * w < (v + y) * z + (x + y) * w.
rewrite the current goal using add_SNo_com((x + y) * z)((v + y) * w)Lxyz(SNo_mul_SNo(v + y)wLvyHw1) (from left to right).
rewrite the current goal using add_SNo_com((v + y) * z)((x + y) * w)(SNo_mul_SNo(v + y)zLvyHz)Lxyw (from left to right).
We will prove(v + y) * w + (x + y) * z < (x + y) * w + (v + y) * z.
Applymul_SNo_Lt(x + y)w(v + y)zLxyHw1LvyHz to the current goal.
An exact proof term for the current goal is SNo_mul_SNoywHyHw1.
We prove the intermediate claimLuyz: SNo(u + y * z).
An exact proof term for the current goal is SNo_add_SNou(y * z)Hu1Lyz.
We prove the intermediate claimLvwyw: SNo(v * w + y * w).
An exact proof term for the current goal is SNo_add_SNo(v * w)(y * w)LvwLyw.
We will prove(x + y) * z < u + y * z.
Applyadd_SNo_Lt1_cancel((x + y) * z)(v * w + y * w)(u + y * z)LxyzLvwywLuyz to the current goal.
We will prove(x + y) * z + v * w + y * w < (u + y * z) + v * w + y * w.
rewrite the current goal using add_SNo_com_4_inner_midu(y * z)(v * w)(y * w)Hu1LyzLvwLyw (from left to right).
We will prove(x + y) * z + v * w + y * w < (u + v * w) + y * z + y * w.
ApplySNoLtLe_tra((x + y) * z + v * w + y * w)(v * z + y * z + x * w + y * w)((u + v * w) + y * z + y * w)(SNo_add_SNo_3((x + y) * z)(v * w)(y * w)LxyzLvwLyw)(SNo_add_SNo_4(v * z)(y * z)(x * w)(y * w)LvzLyzLxwLyw)(SNo_add_SNo_3(u + v * w)(y * z)(y * w)LuvwLyzLyw) to the current goal.
We will prove(x + y) * z + v * w + y * w < v * z + y * z + x * w + y * w.
rewrite the current goal using IHzw(SNoL_SNoSzHzwHw) (from right to left).
We will prove(x + y) * z + v * w + y * w < v * z + y * z + (x + y) * w.
rewrite the current goal using IHxzv(SNoR_SNoSxHxvHv)w(SNoL_SNoSzHzwHw) (from right to left).
We will prove(x + y) * z + (v + y) * w < v * z + y * z + (x + y) * w.
rewrite the current goal using add_SNo_assoc(v * z)(y * z)((x + y) * w)LvzLyzLxyw (from left to right).
rewrite the current goal using IHxv(SNoR_SNoSxHxvHv) (from right to left).
We will prove(x + y) * z + (v + y) * w < (v + y) * z + (x + y) * w.
Applymul_SNo_Lt(v + y)z(x + y)wLvyHzLxyHw1 to the current goal.
An exact proof term for the current goal is SNo_mul_SNoywHyHw1.
We prove the intermediate claimLuxz: SNo(u + x * z).
An exact proof term for the current goal is SNo_add_SNou(x * z)Hu1Lxz.
We prove the intermediate claimLvwxw: SNo(v * w + x * w).
An exact proof term for the current goal is SNo_add_SNo(v * w)(x * w)LvwLxw.
We will prove(x + y) * z < u + x * z.
Applyadd_SNo_Lt1_cancel((x + y) * z)(v * w + x * w)(u + x * z)LxyzLvwxwLuxz to the current goal.
We will prove(x + y) * z + v * w + x * w < (u + x * z) + v * w + x * w.
rewrite the current goal using add_SNo_com_4_inner_midu(x * z)(v * w)(x * w)Hu1LxzLvwLxw (from left to right).
We will prove(x + y) * z + v * w + x * w < (u + v * w) + x * z + x * w.
ApplySNoLtLe_tra((x + y) * z + v * w + x * w)(v * z + x * z + x * w + y * w)((u + v * w) + x * z + x * w)(SNo_add_SNo_3((x + y) * z)(v * w)(x * w)LxyzLvwLxw)(SNo_add_SNo_4(v * z)(x * z)(x * w)(y * w)LvzLxzLxwLyw)(SNo_add_SNo_3(u + v * w)(x * z)(x * w)LuvwLxzLxw) to the current goal.
We will prove(x + y) * z + v * w + x * w < v * z + x * z + x * w + y * w.
rewrite the current goal using IHzw(SNoR_SNoSzHzwHw) (from right to left).
We will prove(x + y) * z + v * w + x * w < v * z + x * z + (x + y) * w.
rewrite the current goal using add_SNo_com(v * w)(x * w)LvwLxw (from left to right).
rewrite the current goal using IHyzv(SNoL_SNoSyHyvHv)w(SNoR_SNoSzHzwHw) (from right to left).
We will prove(x + y) * z + (x + v) * w < v * z + x * z + (x + y) * w.
rewrite the current goal using add_SNo_assoc(v * z)(x * z)((x + y) * w)LvzLxzLxyw (from left to right).
We will prove(x + y) * z + (x + v) * w < (v * z + x * z) + (x + y) * w.
rewrite the current goal using add_SNo_com(v * z)(x * z)LvzLxz (from left to right).
We will prove(x + y) * z + (x + v) * w < (x * z + v * z) + (x + y) * w.
rewrite the current goal using IHyv(SNoL_SNoSyHyvHv) (from right to left).
We will prove(x + y) * z + (x + v) * w < (x + v) * z + (x + y) * w.
rewrite the current goal using add_SNo_com((x + y) * z)((x + v) * w)Lxyz(SNo_mul_SNo(x + v)wLxvHw1) (from left to right).
rewrite the current goal using add_SNo_com((x + v) * z)((x + y) * w)(SNo_mul_SNo(x + v)zLxvHz)Lxyw (from left to right).
We will prove(x + v) * w + (x + y) * z < (x + y) * w + (x + v) * z.
Applymul_SNo_Lt(x + y)w(x + v)zLxyHw1LxvHz to the current goal.
An exact proof term for the current goal is SNo_mul_SNoywHyHw1.
We prove the intermediate claimLuxz: SNo(u + x * z).
An exact proof term for the current goal is SNo_add_SNou(x * z)Hu1Lxz.
We prove the intermediate claimLvwxw: SNo(v * w + x * w).
An exact proof term for the current goal is SNo_add_SNo(v * w)(x * w)LvwLxw.
We prove the intermediate claimLvzxw: SNo(v * z + x * w).
An exact proof term for the current goal is SNo_add_SNo(v * z)(x * w)LvzLxw.
We will prove(x + y) * z < u + x * z.
Applyadd_SNo_Lt1_cancel((x + y) * z)(v * w + x * w)(u + x * z)LxyzLvwxwLuxz to the current goal.
We will prove(x + y) * z + v * w + x * w < (u + x * z) + v * w + x * w.
rewrite the current goal using add_SNo_com_4_inner_midu(x * z)(v * w)(x * w)Hu1LxzLvwLxw (from left to right).
We will prove(x + y) * z + v * w + x * w < (u + v * w) + x * z + x * w.
ApplySNoLtLe_tra((x + y) * z + v * w + x * w)(v * z + x * z + x * w + y * w)((u + v * w) + x * z + x * w)(SNo_add_SNo_3((x + y) * z)(v * w)(x * w)LxyzLvwLxw)(SNo_add_SNo_4(v * z)(x * z)(x * w)(y * w)LvzLxzLxwLyw)(SNo_add_SNo_3(u + v * w)(x * z)(x * w)LuvwLxzLxw) to the current goal.
We will prove(x + y) * z + v * w + x * w < v * z + x * z + x * w + y * w.
rewrite the current goal using IHzw(SNoL_SNoSzHzwHw) (from right to left).
We will prove(x + y) * z + v * w + x * w < v * z + x * z + (x + y) * w.
rewrite the current goal using add_SNo_com(v * w)(x * w)LvwLxw (from left to right).
We will prove(x + y) * z + x * w + v * w < v * z + x * z + (x + y) * w.
rewrite the current goal using IHyzv(SNoR_SNoSyHyvHv)w(SNoL_SNoSzHzwHw) (from right to left).
We will prove(x + y) * z + (x + v) * w < v * z + x * z + (x + y) * w.
rewrite the current goal using add_SNo_assoc(v * z)(x * z)((x + y) * w)LvzLxzLxyw (from left to right).
We will prove(x + y) * z + (x + v) * w < (v * z + x * z) + (x + y) * w.
rewrite the current goal using add_SNo_com(v * z)(x * z)LvzLxz (from left to right).
rewrite the current goal using IHyv(SNoR_SNoSyHyvHv) (from right to left).
We will prove(x + y) * z + (x + v) * w < (x + v) * z + (x + y) * w.
rewrite the current goal using add_SNo_com((x + v) * z)((x + y) * w)(SNo_mul_SNo(x + v)zLxvHz)Lxyw (from left to right).
rewrite the current goal using add_SNo_com((x + y) * z)((x + v) * w)Lxyz(SNo_mul_SNo(x + v)wLxvHw1) (from left to right).
We will prove(x + v) * w + (x + y) * z < (x + y) * w + (x + v) * z.
rewrite the current goal using add_SNo_com((x + v) * w)((x + y) * z)(SNo_mul_SNo(x + v)wLxvHw1)Lxyz (from left to right).
rewrite the current goal using add_SNo_com((x + y) * w)((x + v) * z)Lxyw(SNo_mul_SNo(x + v)zLxvHz) (from left to right).
We will prove(x + y) * z + (x + v) * w < (x + v) * z + (x + y) * w.
Applymul_SNo_Lt(x + v)z(x + y)wLxvHzLxyHw1 to the current goal.
HypothesisDL : ∀x y z, SNox → SNoy → SNoz → x * (y + z) = x * y + x * z
HypothesisDR : ∀x y z, SNox → SNoy → SNoz → (x + y) * z = x * z + y * z
HypothesisIL : ∀x y, SNox → SNoy → ∀u ∈ SNoL(x * y), ∀p : prop, (∀v ∈ SNoLx, ∀w ∈ SNoLy, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoRx, ∀w ∈ SNoRy, u + v * w ≤ v * y + x * w → p) → p
HypothesisIR : ∀x y, SNox → SNoy → ∀u ∈ SNoR(x * y), ∀p : prop, (∀v ∈ SNoLx, ∀w ∈ SNoRy, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoRx, ∀w ∈ SNoLy, v * y + x * w ≤ u + v * w → p) → p
HypothesisM_Lt : ∀x y u v, SNox → SNoy → SNou → SNov → u < x → v < y → u * y + x * v < x * y + u * v
HypothesisM_Le : ∀x y u v, SNox → SNoy → SNou → SNov → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v
An exact proof term for the current goal is SNo_MyzHyHz.
We prove the intermediate claimLxyz2: SNo((x * y) * z).
An exact proof term for the current goal is SNo_M(x * y)zLxyHz.
We prove the intermediate claimL1: ∀v ∈ SNoS_(SNoLevx), ∀w, SNow → ∀w1 ∈ SNoS_(SNoLevy), ∀w2 ∈ SNoS_(SNoLevz), u = v * (y * z) + x * w + - v * w → v * (w1 * z + y * w2) + x * (w + w1 * w2) ≤ x * (w1 * z + y * w2) + v * (w + w1 * w2) → (v * y + x * w1) * z + (x * y + v * w1) * w2 < (x * y + v * w1) * z + (v * y + x * w1) * w2 → u < (x * y) * z.
An exact proof term for the current goal is SNo_Myw2HyHw23.
We prove the intermediate claimLvw1z: SNo(v * (w1 * z)).
An exact proof term for the current goal is SNo_Mv(w1 * z)Hv3Lw1z.
We prove the intermediate claimLvyw2: SNo(v * (y * w2)).
An exact proof term for the current goal is SNo_Mv(y * w2)Hv3Lyw2.
We prove the intermediate claimLw1w2: SNo(w1 * w2).
An exact proof term for the current goal is SNo_Mw1w2Hw13Hw23.
We prove the intermediate claimLxw1w2: SNo(x * (w1 * w2)).
An exact proof term for the current goal is SNo_Mx(w1 * w2)HxLw1w2.
We prove the intermediate claimLxw1z: SNo(x * (w1 * z)).
An exact proof term for the current goal is SNo_Mx(w1 * z)HxLw1z.
We prove the intermediate claimLxyw2: SNo(x * (y * w2)).
An exact proof term for the current goal is SNo_Mx(y * w2)HxLyw2.
We prove the intermediate claimLvyzxw: SNo(v * (y * z) + x * w).
An exact proof term for the current goal is SNo_add_SNo(v * (y * z))(x * w)LvyzLxw.
We prove the intermediate claimLxyzvw: SNo((x * y) * z + v * w).
An exact proof term for the current goal is SNo_add_SNo((x * y) * z)(v * w)Lxyz2Lvw.
We prove the intermediate claimLvw1w2: SNo(v * (w1 * w2)).
An exact proof term for the current goal is SNo_Mv(w1 * w2)Hv3Lw1w2.
We prove the intermediate claimLww1w2: SNo(w + w1 * w2).
An exact proof term for the current goal is SNo_add_SNow(w1 * w2)HwLw1w2.
We prove the intermediate claimLvww1w2: SNo(v * (w + w1 * w2)).
An exact proof term for the current goal is SNo_Mv(w + w1 * w2)Hv3Lww1w2.
We prove the intermediate claimLvw1zyw2: SNo(v * (w1 * z + y * w2)).
An exact proof term for the current goal is SNo_Mv(w1 * z + y * w2)Hv3(SNo_add_SNo(w1 * z)(y * w2)Lw1zLyw2).
We prove the intermediate claimLvwvw1w2: SNo(v * w + v * (w1 * w2)).
An exact proof term for the current goal is SNo_add_SNo(v * w)(v * (w1 * w2))LvwLvw1w2.
We prove the intermediate claimLvyzxw1zxyw2vwvw1w2: SNo(v * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2)).
An exact proof term for the current goal is SNo_add_SNo_4(v * (y * z))(x * (w1 * z))(x * (y * w2))(v * w + v * (w1 * w2))LvyzLxw1zLxyw2Lvwvw1w2.
We prove the intermediate claimLvw1zvyw2xw1w2: SNo(v * (w1 * z) + v * (y * w2) + x * (w1 * w2)).
An exact proof term for the current goal is SNo_add_SNo_3(v * (w1 * z))(v * (y * w2))(x * (w1 * w2))Lvw1zLvyw2Lxw1w2.
We will proveu < (x * y) * z.
rewrite the current goal using Hue (from left to right).
We will prove(v * (y * z)) + (x * w) + - (v * w) < (x * y) * z.
Applyadd_SNo_minus_Lt1b3(v * (y * z))(x * w)(v * w)((x * y) * z)LvyzLxwLvwLxyz2 to the current goal.
We will provev * (y * z) + x * w < (x * y) * z + v * w.
Applyadd_SNo_Lt1_cancel(v * (y * z) + x * w)(v * (w1 * z) + v * (y * w2) + x * (w1 * w2))((x * y) * z + v * w)LvyzxwLvw1zvyw2xw1w2Lxyzvw to the current goal.
We will prove(v * (y * z) + x * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2) < ((x * y) * z + v * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2).
ApplySNoLeLt_tra((v * (y * z) + x * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2))(v * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2))(((x * y) * z + v * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2)) to the current goal.
An exact proof term for the current goal is Lxyzvw.
An exact proof term for the current goal is Lvw1zvyw2xw1w2.
We will prove(v * (y * z) + x * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2) ≤ v * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2).
rewrite the current goal using add_SNo_assoc(v * (y * z))(x * w)(v * (w1 * z) + v * (y * w2) + x * (w1 * w2))LvyzLxwLvw1zvyw2xw1w2 (from right to left).
We will provev * (y * z) + x * w + v * (w1 * z) + v * (y * w2) + x * (w1 * w2) ≤ v * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2).
Applyadd_SNo_Le2(v * (y * z))(x * w + v * (w1 * z) + v * (y * w2) + x * (w1 * w2))(x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2))Lvyz(SNo_add_SNo(x * w)(v * (w1 * z) + v * (y * w2) + x * (w1 * w2))LxwLvw1zvyw2xw1w2)(SNo_add_SNo_4(x * (w1 * z))(x * (y * w2))(v * w)(v * (w1 * w2))Lxw1zLxyw2LvwLvw1w2) to the current goal.
We will provex * w + v * (w1 * z) + v * (y * w2) + x * (w1 * w2) ≤ x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2).
rewrite the current goal using add_SNo_assoc(v * (w1 * z))(v * (y * w2))(x * (w1 * w2))Lvw1zLvyw2Lxw1w2 (from left to right).
rewrite the current goal using DLv(w1 * z)(y * w2)Hv3Lw1zLyw2 (from right to left).
We will provex * w + v * (w1 * z + y * w2) + x * (w1 * w2) ≤ x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2).
rewrite the current goal using add_SNo_com_3_0_1(x * w)(v * (w1 * z + y * w2))(x * (w1 * w2))LxwLvw1zyw2Lxw1w2 (from left to right).
We will provev * (w1 * z + y * w2) + x * w + x * (w1 * w2) ≤ x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2).
rewrite the current goal using DLxw(w1 * w2)HxHwLw1w2 (from right to left).
We will provev * (w1 * z + y * w2) + x * (w + w1 * w2) ≤ x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2).
rewrite the current goal using DLvw(w1 * w2)Hv3HwLw1w2 (from right to left).
We will provev * (w1 * z + y * w2) + x * (w + w1 * w2) ≤ x * (w1 * z) + x * (y * w2) + v * (w + w1 * w2).
rewrite the current goal using add_SNo_assoc(x * (w1 * z))(x * (y * w2))(v * (w + w1 * w2))Lxw1zLxyw2Lvww1w2 (from left to right).
rewrite the current goal using DLx(w1 * z)(y * w2)HxLw1zLyw2 (from right to left).
We will provev * (w1 * z + y * w2) + x * (w + w1 * w2) ≤ x * (w1 * z + y * w2) + v * (w + w1 * w2).
An exact proof term for the current goal is H1.
We will provev * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2) < ((x * y) * z + v * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2).
rewrite the current goal using add_SNo_com((x * y) * z)(v * w)Lxyz2Lvw (from left to right).
rewrite the current goal using add_SNo_assoc(v * w)((x * y) * z)(v * (w1 * z) + v * (y * w2) + x * (w1 * w2))LvwLxyz2Lvw1zvyw2xw1w2 (from right to left).
We will provev * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2) < v * w + (x * y) * z + v * (w1 * z) + v * (y * w2) + x * (w1 * w2).
rewrite the current goal using add_SNo_rotate_5_2(v * (y * z))(x * (w1 * z))(x * (y * w2))(v * w)(v * (w1 * w2))LvyzLxw1zLxyw2LvwLvw1w2 (from left to right).
We will provev * w + v * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2) < v * w + (x * y) * z + v * (w1 * z) + v * (y * w2) + x * (w1 * w2).
Applyadd_SNo_Lt2(v * w)(v * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2))((x * y) * z + v * (w1 * z) + v * (y * w2) + x * (w1 * w2))Lvw(SNo_add_SNo_4(v * (w1 * w2))(v * (y * z))(x * (w1 * z))(x * (y * w2))Lvw1w2LvyzLxw1zLxyw2)(SNo_add_SNo_4((x * y) * z)(v * (w1 * z))(v * (y * w2))(x * (w1 * w2))Lxyz2Lvw1zLvyw2Lxw1w2) to the current goal.
We will provev * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2) < (x * y) * z + v * (w1 * z) + v * (y * w2) + x * (w1 * w2).
rewrite the current goal using add_SNo_assoc((x * y) * z)(v * (w1 * z))(v * (y * w2) + x * (w1 * w2))Lxyz2Lvw1z(SNo_add_SNo(v * (y * w2))(x * (w1 * w2))Lvyw2Lxw1w2) (from left to right).
We will provev * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2) < ((x * y) * z + v * (w1 * z)) + v * (y * w2) + x * (w1 * w2).
rewrite the current goal using IHxzvHvw2Hw2 (from left to right).
rewrite the current goal using IHyzw1Hw1w2Hw2 (from left to right).
We will provev * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2) < ((x * y) * z + v * (w1 * z)) + (v * y) * w2 + (x * w1) * w2.
rewrite the current goal using DR(v * y)(x * w1)w2LvyLxw1Hw23 (from right to left).
We will provev * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2) < ((x * y) * z + v * (w1 * z)) + (v * y + x * w1) * w2.
rewrite the current goal using IHxyvHvw1Hw1 (from left to right).
rewrite the current goal using DR(x * y)(v * w1)zLxyLvw1Hz (from right to left).
We will provev * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2) < (x * y + v * w1) * z + (v * y + x * w1) * w2.
rewrite the current goal using add_SNo_rotate_4_1(v * (y * z))(x * (w1 * z))(x * (y * w2))(v * (w1 * w2))LvyzLxw1zLxyw2Lvw1w2 (from right to left).
We will provev * (y * z) + x * (w1 * z) + x * (y * w2) + v * (w1 * w2) < (x * y + v * w1) * z + (v * y + x * w1) * w2.
rewrite the current goal using add_SNo_assoc(v * (y * z))(x * (w1 * z))(x * (y * w2) + v * (w1 * w2))LvyzLxw1z(SNo_add_SNo(x * (y * w2))(v * (w1 * w2))Lxyw2Lvw1w2) (from left to right).
We will prove(v * (y * z) + x * (w1 * z)) + x * (y * w2) + v * (w1 * w2) < (x * y + v * w1) * z + (v * y + x * w1) * w2.
rewrite the current goal using IHxvHv (from left to right).
rewrite the current goal using IHyw1Hw1 (from left to right).
rewrite the current goal using IHzw2Hw2 (from left to right).
rewrite the current goal using IHxyzvHvw1Hw1w2Hw2 (from left to right).
We will prove((v * y) * z + (x * w1) * z) + (x * y) * w2 + (v * w1) * w2 < (x * y + v * w1) * z + (v * y + x * w1) * w2.
rewrite the current goal using DR(v * y)(x * w1)zLvyLxw1Hz (from right to left).
rewrite the current goal using DR(x * y)(v * w1)w2LxyLvw1Hw23 (from right to left).
We will prove(v * y + x * w1) * z + (x * y + v * w1) * w2 < (x * y + v * w1) * z + (v * y + x * w1) * w2.
We will prove(v * y + x * w1) * z + (x * y + v * w1) * w2 < (x * y + v * w1) * z + (v * y + x * w1) * w2.
ApplyM_Lt(x * y + v * w1)z(v * y + x * w1)w2(SNo_add_SNo(x * y)(v * w1)Lxy(SNo_Mvw1Hv1Hw11))Hz(SNo_add_SNo(v * y)(x * w1)(SNo_MvyHv1Hy)(SNo_Mxw1HxHw11))Hw21 to the current goal.
An exact proof term for the current goal is SNo_MyzHyHz.
We prove the intermediate claimLxyz2: SNo((x * y) * z).
An exact proof term for the current goal is SNo_M(x * y)zLxyHz.
We prove the intermediate claimL2: ∀v ∈ SNoS_(SNoLevx), ∀w, SNow → ∀w1 ∈ SNoS_(SNoLevy), ∀w2 ∈ SNoS_(SNoLevz), u = v * (y * z) + x * w + - v * w → x * (w1 * z + y * w2) + v * (w + w1 * w2) ≤ v * (w1 * z + y * w2) + x * (w + w1 * w2) → (x * y + v * w1) * z + (v * y + x * w1) * w2 < (v * y + x * w1) * z + (x * y + v * w1) * w2 → (x * y) * z < u.
An exact proof term for the current goal is SNo_Myw2HyHw23.
We prove the intermediate claimLvw1z: SNo(v * (w1 * z)).
An exact proof term for the current goal is SNo_Mv(w1 * z)Hv3Lw1z.
We prove the intermediate claimLvyw2: SNo(v * (y * w2)).
An exact proof term for the current goal is SNo_Mv(y * w2)Hv3Lyw2.
We prove the intermediate claimLw1w2: SNo(w1 * w2).
An exact proof term for the current goal is SNo_Mw1w2Hw13Hw23.
We prove the intermediate claimLxw1w2: SNo(x * (w1 * w2)).
An exact proof term for the current goal is SNo_Mx(w1 * w2)HxLw1w2.
We prove the intermediate claimLxw1z: SNo(x * (w1 * z)).
An exact proof term for the current goal is SNo_Mx(w1 * z)HxLw1z.
We prove the intermediate claimLxyw2: SNo(x * (y * w2)).
An exact proof term for the current goal is SNo_Mx(y * w2)HxLyw2.
We prove the intermediate claimLvyzxw: SNo(v * (y * z) + x * w).
An exact proof term for the current goal is SNo_add_SNo(v * (y * z))(x * w)LvyzLxw.
We prove the intermediate claimLxyzvw: SNo((x * y) * z + v * w).
An exact proof term for the current goal is SNo_add_SNo((x * y) * z)(v * w)Lxyz2Lvw.
We prove the intermediate claimLvw1w2: SNo(v * (w1 * w2)).
An exact proof term for the current goal is SNo_Mv(w1 * w2)Hv3Lw1w2.
We prove the intermediate claimLww1w2: SNo(w + w1 * w2).
An exact proof term for the current goal is SNo_add_SNow(w1 * w2)HwLw1w2.
We prove the intermediate claimLvww1w2: SNo(v * (w + w1 * w2)).
An exact proof term for the current goal is SNo_Mv(w + w1 * w2)Hv3Lww1w2.
We prove the intermediate claimLvw1zyw2: SNo(v * (w1 * z + y * w2)).
An exact proof term for the current goal is SNo_Mv(w1 * z + y * w2)Hv3(SNo_add_SNo(w1 * z)(y * w2)Lw1zLyw2).
We prove the intermediate claimLvwvw1w2: SNo(v * w + v * (w1 * w2)).
An exact proof term for the current goal is SNo_add_SNo(v * w)(v * (w1 * w2))LvwLvw1w2.
We prove the intermediate claimLvyzxw1zxyw2vwvw1w2: SNo(v * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2)).
An exact proof term for the current goal is SNo_add_SNo_4(v * (y * z))(x * (w1 * z))(x * (y * w2))(v * w + v * (w1 * w2))LvyzLxw1zLxyw2Lvwvw1w2.
We prove the intermediate claimLvw1zvyw2xw1w2: SNo(v * (w1 * z) + v * (y * w2) + x * (w1 * w2)).
An exact proof term for the current goal is SNo_add_SNo_3(v * (w1 * z))(v * (y * w2))(x * (w1 * w2))Lvw1zLvyw2Lxw1w2.
rewrite the current goal using Hue (from left to right).
Applyadd_SNo_minus_Lt2b3(v * (y * z))(x * w)(v * w)((x * y) * z)LvyzLxwLvwLxyz2 to the current goal.
We will prove(x * y) * z + v * w < v * (y * z) + x * w.
Applyadd_SNo_Lt1_cancel((x * y) * z + v * w)(v * (w1 * z) + v * (y * w2) + x * (w1 * w2))(v * (y * z) + x * w)LxyzvwLvw1zvyw2xw1w2Lvyzxw to the current goal.
We will prove((x * y) * z + v * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2) < (v * (y * z) + x * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2).
ApplySNoLtLe_tra(((x * y) * z + v * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2))(v * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2))((v * (y * z) + x * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2)) to the current goal.
An exact proof term for the current goal is Lvyzxw.
An exact proof term for the current goal is Lvw1zvyw2xw1w2.
We will prove((x * y) * z + v * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2) < v * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2).
rewrite the current goal using add_SNo_com((x * y) * z)(v * w)Lxyz2Lvw (from left to right).
rewrite the current goal using add_SNo_assoc(v * w)((x * y) * z)(v * (w1 * z) + v * (y * w2) + x * (w1 * w2))LvwLxyz2Lvw1zvyw2xw1w2 (from right to left).
We will provev * w + (x * y) * z + v * (w1 * z) + v * (y * w2) + x * (w1 * w2) < v * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2).
rewrite the current goal using add_SNo_rotate_5_2(v * (y * z))(x * (w1 * z))(x * (y * w2))(v * w)(v * (w1 * w2))LvyzLxw1zLxyw2LvwLvw1w2 (from left to right).
We will provev * w + (x * y) * z + v * (w1 * z) + v * (y * w2) + x * (w1 * w2) < v * w + v * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2).
Applyadd_SNo_Lt2(v * w)((x * y) * z + v * (w1 * z) + v * (y * w2) + x * (w1 * w2))(v * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2))Lvw(SNo_add_SNo_4((x * y) * z)(v * (w1 * z))(v * (y * w2))(x * (w1 * w2))Lxyz2Lvw1zLvyw2Lxw1w2)(SNo_add_SNo_4(v * (w1 * w2))(v * (y * z))(x * (w1 * z))(x * (y * w2))Lvw1w2LvyzLxw1zLxyw2) to the current goal.
We will prove(x * y) * z + v * (w1 * z) + v * (y * w2) + x * (w1 * w2) < v * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2).
rewrite the current goal using add_SNo_assoc((x * y) * z)(v * (w1 * z))(v * (y * w2) + x * (w1 * w2))Lxyz2Lvw1z(SNo_add_SNo(v * (y * w2))(x * (w1 * w2))Lvyw2Lxw1w2) (from left to right).
We will prove((x * y) * z + v * (w1 * z)) + v * (y * w2) + x * (w1 * w2) < v * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2).
rewrite the current goal using IHxzvHvw2Hw2 (from left to right).
rewrite the current goal using IHyzw1Hw1w2Hw2 (from left to right).
We will prove((x * y) * z + v * (w1 * z)) + (v * y) * w2 + (x * w1) * w2 < v * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2).
rewrite the current goal using DR(v * y)(x * w1)w2LvyLxw1Hw23 (from right to left).
We will prove((x * y) * z + v * (w1 * z)) + (v * y + x * w1) * w2 < v * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2).
rewrite the current goal using IHxyvHvw1Hw1 (from left to right).
rewrite the current goal using DR(x * y)(v * w1)zLxyLvw1Hz (from right to left).
We will prove(x * y + v * w1) * z + (v * y + x * w1) * w2 < v * (w1 * w2) + v * (y * z) + x * (w1 * z) + x * (y * w2).
rewrite the current goal using add_SNo_rotate_4_1(v * (y * z))(x * (w1 * z))(x * (y * w2))(v * (w1 * w2))LvyzLxw1zLxyw2Lvw1w2 (from right to left).
We will prove(x * y + v * w1) * z + (v * y + x * w1) * w2 < v * (y * z) + x * (w1 * z) + x * (y * w2) + v * (w1 * w2).
rewrite the current goal using add_SNo_assoc(v * (y * z))(x * (w1 * z))(x * (y * w2) + v * (w1 * w2))LvyzLxw1z(SNo_add_SNo(x * (y * w2))(v * (w1 * w2))Lxyw2Lvw1w2) (from left to right).
We will prove(x * y + v * w1) * z + (v * y + x * w1) * w2 < (v * (y * z) + x * (w1 * z)) + x * (y * w2) + v * (w1 * w2).
rewrite the current goal using IHxvHv (from left to right).
rewrite the current goal using IHyw1Hw1 (from left to right).
rewrite the current goal using IHzw2Hw2 (from left to right).
rewrite the current goal using IHxyzvHvw1Hw1w2Hw2 (from left to right).
We will prove(x * y + v * w1) * z + (v * y + x * w1) * w2 < ((v * y) * z + (x * w1) * z) + (x * y) * w2 + (v * w1) * w2.
rewrite the current goal using DR(v * y)(x * w1)zLvyLxw1Hz (from right to left).
rewrite the current goal using DR(x * y)(v * w1)w2LxyLvw1Hw23 (from right to left).
We will prove(x * y + v * w1) * z + (v * y + x * w1) * w2 < (v * y + x * w1) * z + (x * y + v * w1) * w2.
An exact proof term for the current goal is H2.
We will provev * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2) ≤ (v * (y * z) + x * w) + v * (w1 * z) + v * (y * w2) + x * (w1 * w2).
rewrite the current goal using add_SNo_assoc(v * (y * z))(x * w)(v * (w1 * z) + v * (y * w2) + x * (w1 * w2))LvyzLxwLvw1zvyw2xw1w2 (from right to left).
We will provev * (y * z) + x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2) ≤ v * (y * z) + x * w + v * (w1 * z) + v * (y * w2) + x * (w1 * w2).
Applyadd_SNo_Le2(v * (y * z))(x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2))(x * w + v * (w1 * z) + v * (y * w2) + x * (w1 * w2))Lvyz(SNo_add_SNo_4(x * (w1 * z))(x * (y * w2))(v * w)(v * (w1 * w2))Lxw1zLxyw2LvwLvw1w2)(SNo_add_SNo(x * w)(v * (w1 * z) + v * (y * w2) + x * (w1 * w2))LxwLvw1zvyw2xw1w2) to the current goal.
We will provex * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2) ≤ x * w + v * (w1 * z) + v * (y * w2) + x * (w1 * w2).
rewrite the current goal using add_SNo_assoc(v * (w1 * z))(v * (y * w2))(x * (w1 * w2))Lvw1zLvyw2Lxw1w2 (from left to right).
rewrite the current goal using DLv(w1 * z)(y * w2)Hv3Lw1zLyw2 (from right to left).
We will provex * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2) ≤ x * w + v * (w1 * z + y * w2) + x * (w1 * w2).
rewrite the current goal using add_SNo_com_3_0_1(x * w)(v * (w1 * z + y * w2))(x * (w1 * w2))LxwLvw1zyw2Lxw1w2 (from left to right).
We will provex * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2) ≤ v * (w1 * z + y * w2) + x * w + x * (w1 * w2).
rewrite the current goal using DLxw(w1 * w2)HxHwLw1w2 (from right to left).
We will provex * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2) ≤ v * (w1 * z + y * w2) + x * (w + w1 * w2).
rewrite the current goal using DLvw(w1 * w2)Hv3HwLw1w2 (from right to left).
We will provex * (w1 * z) + x * (y * w2) + v * (w + w1 * w2) ≤ v * (w1 * z + y * w2) + x * (w + w1 * w2).
rewrite the current goal using add_SNo_assoc(x * (w1 * z))(x * (y * w2))(v * (w + w1 * w2))Lxw1zLxyw2Lvww1w2 (from left to right).
rewrite the current goal using DLx(w1 * z)(y * w2)HxLw1zLyw2 (from right to left).
We will provex * (w1 * z + y * w2) + v * (w + w1 * w2) ≤ v * (w1 * z + y * w2) + x * (w + w1 * w2).
We will prove(x * y + v * w1) * z + (v * y + x * w1) * w2 < (v * y + x * w1) * z + (x * y + v * w1) * w2.
rewrite the current goal using add_SNo_com((v * y + x * w1) * z)((x * y + v * w1) * w2)Lvyxw1zLxyvw1w2 (from left to right).
rewrite the current goal using add_SNo_com((x * y + v * w1) * z)((v * y + x * w1) * w2)Lxyvw1zLvyxw1w2 (from left to right).
We will prove(v * y + x * w1) * w2 + (x * y + v * w1) * z < (x * y + v * w1) * w2 + (v * y + x * w1) * z.
ApplyM_Lt(x * y + v * w1)w2(v * y + x * w1)z(SNo_add_SNo(x * y)(v * w1)Lxy(SNo_Mvw1Hv1Hw11))Hw21(SNo_add_SNo(v * y)(x * w1)(SNo_MvyHv1Hy)(SNo_Mxw1HxHw11))Hz to the current goal.
We prove the intermediate claimLIL': ∀x y, SNox → SNoy → ∀u ∈ SNoL(y * x), ∀p : prop, (∀v ∈ SNoLx, ∀w ∈ SNoLy, u + w * v ≤ y * v + w * x → p) → (∀v ∈ SNoRx, ∀w ∈ SNoRy, u + w * v ≤ y * v + w * x → p) → p.
An exact proof term for the current goal is Hp2vHvwHw.
We prove the intermediate claimLIR': ∀x y, SNox → SNoy → ∀u ∈ SNoR(y * x), ∀p : prop, (∀v ∈ SNoLx, ∀w ∈ SNoRy, y * v + w * x ≤ u + w * v → p) → (∀v ∈ SNoRx, ∀w ∈ SNoLy, y * v + w * x ≤ u + w * v → p) → p.
rewrite the current goal using HE (from right to left).
We will prove∀u ∈ L', u < x * (y * z).
Applymul_SNo_assoc_lem1(λx y ⇒ y * x)(λx y Hx Hy ⇒ SNo_mul_SNoyxHyHx)(λx y z Hx Hy Hz ⇒ mul_SNo_distrRyzxHyHzHx)(λx y z Hx Hy Hz ⇒ mul_SNo_distrLzxyHzHxHy)LIL'LIR'LMLt'LMLe'zyxHzHyHxLIHz'LIHy'LIHx'LIHzy'LIHzx'LIHyx'LIHzyx' to the current goal.
We will prove∀u ∈ L', ∀q : prop, (∀v ∈ SNoLz, ∀w ∈ SNoL(x * y), u = (x * y) * v + w * z + - w * v → q) → (∀v ∈ SNoRz, ∀w ∈ SNoR(x * y), u = (x * y) * v + w * z + - w * v → q) → q.
An exact proof term for the current goal is Hq2vHvwHw.
rewrite the current goal using HE (from right to left).
We will prove∀u ∈ R', x * (y * z) < u.
Applymul_SNo_assoc_lem2(λx y ⇒ y * x)(λx y Hx Hy ⇒ SNo_mul_SNoyxHyHx)(λx y z Hx Hy Hz ⇒ mul_SNo_distrRyzxHyHzHx)(λx y z Hx Hy Hz ⇒ mul_SNo_distrLzxyHzHxHy)LIL'LIR'LMLt'LMLe'zyxHzHyHxLIHz'LIHy'LIHx'LIHzy'LIHzx'LIHyx'LIHzyx' to the current goal.
We will prove∀u ∈ R', ∀q : prop, (∀v ∈ SNoLz, ∀w ∈ SNoR(x * y), u = (x * y) * v + w * z + - w * v → q) → (∀v ∈ SNoRz, ∀w ∈ SNoL(x * y), u = (x * y) * v + w * z + - w * v → q) → q.