Set P to be the term λx y z ⇒ (x + y) * z = x * z + y * z of type set → set → set → prop.
We will prove ∀x y z, SNo x → SNo y → SNo z → P x y z.
Apply SNoLev_ind3 P to the current goal.
Let x, y and z be given.
Assume Hx Hy Hz.
Assume IHx: ∀u ∈ SNoS_ (SNoLev x), (u + y) * z = u * z + y * z.
Assume IHy: ∀v ∈ SNoS_ (SNoLev y), (x + v) * z = x * z + v * z.
Assume IHz: ∀w ∈ SNoS_ (SNoLev z), (x + y) * w = x * w + y * w.
Assume IHxy: ∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), (u + v) * z = u * z + v * z.
Assume IHxz: ∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), (u + y) * w = u * w + y * w.
Assume IHyz: ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), (x + v) * w = x * w + v * w.
Assume IHxyz: ∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), (u + v) * w = u * w + v * w.
We will prove (x + y) * z = x * z + y * z.
Apply mul_SNo_eq_3 (x + y) z (SNo_add_SNo x y Hx Hy) Hz to the current goal.
Let L and R be given.
Assume HLR HLE HLI1 HLI2 HRE HRI1 HRI2.
Assume HE: (x + y) * z = SNoCut L R.
Set L1 to be the term {w + y * z|w ∈ SNoL (x * z)}.
Set L2 to be the term {x * z + w|w ∈ SNoL (y * z)}.
Set R1 to be the term {w + y * z|w ∈ SNoR (x * z)}.
Set R2 to be the term {x * z + w|w ∈ SNoR (y * z)}.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim Lxyz: SNo ((x + y) * z).
An exact proof term for the current goal is SNo_mul_SNo (x + y) z Lxy Hz.
We prove the intermediate claim Lxz: SNo (x * z).
An exact proof term for the current goal is SNo_mul_SNo x z Hx Hz.
We prove the intermediate claim Lyz: SNo (y * z).
An exact proof term for the current goal is SNo_mul_SNo y z Hy Hz.
We prove the intermediate claim Lxzyz: SNo (x * z + y * z).
An exact proof term for the current goal is SNo_add_SNo (x * z) (y * z) Lxz Lyz.
We prove the intermediate claim LE: x * z + y * z = SNoCut (L1 ∪ L2) (R1 ∪ R2).
An exact proof term for the current goal is add_SNo_eq (x * z) (SNo_mul_SNo x z Hx Hz) (y * z) (SNo_mul_SNo y z Hy Hz).
rewrite the current goal using HE (from left to right).
rewrite the current goal using LE (from left to right).
Apply SNoCut_ext to the current goal.
An exact proof term for the current goal is HLR.
An exact proof term for the current goal is add_SNo_SNoCutP (x * z) (y * z) (SNo_mul_SNo x z Hx Hz) (SNo_mul_SNo y z Hy Hz).
Let u be given.
Assume Hu: u ∈ L.
rewrite the current goal using LE (from right to left).
We will prove u < x * z + y * z.
Apply HLE u Hu to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL (x + y).
Let w be given.
Assume Hw: w ∈ SNoL z.
Assume Hue: u = v * z + (x + y) * w + - v * w.
rewrite the current goal using Hue (from left to right).
We will prove v * z + (x + y) * w + - v * w < x * z + y * z.
Apply SNoL_E (x + y) Lxy v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoL_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lxwyw: SNo (x * w + y * w).
An exact proof term for the current goal is SNo_add_SNo (x * w) (y * w) Lxw Lyw.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lvzxwyw: SNo (v * z + x * w + y * w).
An exact proof term for the current goal is SNo_add_SNo_3 (v * z) (x * w) (y * w) Lvz Lxw Lyw.
We prove the intermediate claim Lxzyzvw: SNo (x * z + y * z + v * w).
An exact proof term for the current goal is SNo_add_SNo_3 (x * z) (y * z) (v * w) Lxz Lyz Lvw.
Apply add_SNo_minus_Lt1b3 (v * z) ((x + y) * w) (v * w) (x * z + y * z) Lvz Lxyw Lvw Lxzyz to the current goal.
We will prove v * z + (x + y) * w < (x * z + y * z) + v * w.
rewrite the current goal using IHz w (SNoL_SNoS z Hz w Hw) (from left to right).
We will prove v * z + x * w + y * w < (x * z + y * z) + v * w.
rewrite the current goal using add_SNo_assoc (x * z) (y * z) (v * w) Lxz Lyz Lvw (from right to left).
We will prove v * z + x * w + y * w < x * z + y * z + v * w.
Apply add_SNo_SNoL_interpolate x y Hx Hy v Hv to the current goal.
Assume H1.
Apply H1 to the current goal.
Let u be given.
Assume H1.
Apply H1 to the current goal.
Assume Hu: u ∈ SNoL x.
Assume Hvu: v ≤ u + y.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
We prove the intermediate claim Luw: SNo (u * w).
An exact proof term for the current goal is SNo_mul_SNo u w Hu1 Hw1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu1 Hz.
We prove the intermediate claim Luy: SNo (u + y).
An exact proof term for the current goal is SNo_add_SNo u y Hu1 Hy.
Apply add_SNo_Lt1_cancel (v * z + x * w + y * w) (u * w) (x * z + y * z + v * w) Lvzxwyw Luw Lxzyzvw 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) Lvz Lxw Lyw Luw (from right to left).
rewrite the current goal using add_SNo_assoc_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw (from right to left).
We will prove v * z + x * w + y * w + u * w < x * z + y * z + v * w + u * w.
Apply SNoLeLt_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) Lvz Lxw Lyw Luw) (SNo_add_SNo_4 (u * z) (y * z) (v * w) (x * w) Luz Lyz Lvw Lxw) (SNo_add_SNo_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw) to the current goal.
We will prove v * 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) Lvz Lxw (SNo_add_SNo (y * w) (u * w) Lyw Luw) (from left to right).
We will prove x * 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) Luz Lyz Lvw Lxw (from left to right).
We will prove x * w + v * z + y * w + u * w ≤ x * w + u * z + y * z + v * w.
Apply add_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) Lvz Lyw Luw) (SNo_add_SNo_3 (u * z) (y * z) (v * w) Luz Lyz Lvw) to the current goal.
We will prove v * z + y * w + u * w ≤ u * z + y * z + v * w.
rewrite the current goal using add_SNo_com (y * w) (u * w) Lyw Luw (from left to right).
We will prove v * z + u * w + y * w ≤ u * z + y * z + v * w.
rewrite the current goal using IHxz u (SNoL_SNoS x Hx u Hu) w (SNoL_SNoS z Hz w Hw) (from right to left).
We will prove v * z + (u + y) * w ≤ u * z + y * z + v * w.
rewrite the current goal using add_SNo_assoc (u * z) (y * z) (v * w) Luz Lyz Lvw (from left to right).
We will prove v * z + (u + y) * w ≤ (u * z + y * z) + v * w.
rewrite the current goal using IHx u (SNoL_SNoS x Hx u Hu) (from right to left).
We will prove v * z + (u + y) * w ≤ (u + y) * z + v * w.
Apply mul_SNo_Le (u + y) z v w Luy Hz Hv1 Hw1 to the current goal.
We will prove v ≤ u + y.
An exact proof term for the current goal is Hvu.
We will prove w ≤ z.
Apply SNoLtLe to the current goal.
We will prove w < z.
An exact proof term for the current goal is Hw3.
We will prove u * 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) Luz Lyz (SNo_add_SNo (v * w) (x * w) Lvw Lxw) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (x * z) (y * z) (v * w + u * w) Lxz Lyz (SNo_add_SNo (v * w) (u * w) Lvw Luw) (from left to right).
We will prove y * z + u * z + v * w + x * w < y * z + x * z + v * w + u * w.
Apply add_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) Luz Lvw Lxw) (SNo_add_SNo_3 (x * z) (v * w) (u * w) Lxz Lvw Luw) to the current goal.
We will prove u * 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) Luz Lvw Lxw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (x * z) (v * w) (u * w) Lxz Lvw Luw (from left to right).
We will prove v * w + u * z + x * w < v * w + x * z + u * w.
Apply add_SNo_Lt2 (v * w) (u * z + x * w) (x * z + u * w) Lvw (SNo_add_SNo (u * z) (x * w) Luz Lxw) (SNo_add_SNo (x * z) (u * w) Lxz Luw) to the current goal.
We will prove u * z + x * w < x * z + u * w.
An exact proof term for the current goal is mul_SNo_Lt x z u w Hx Hz Hu1 Hw1 Hu3 Hw3.
Assume H1.
Apply H1 to the current goal.
Let u be given.
Assume H1.
Apply H1 to the current goal.
Assume Hu: u ∈ SNoL y.
Assume Hvu: v ≤ x + u.
Apply SNoL_E y Hy u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
We prove the intermediate claim Luw: SNo (u * w).
An exact proof term for the current goal is SNo_mul_SNo u w Hu1 Hw1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu1 Hz.
We prove the intermediate claim Lxu: SNo (x + u).
An exact proof term for the current goal is SNo_add_SNo x u Hx Hu1.
Apply add_SNo_Lt1_cancel (v * z + x * w + y * w) (u * w) (x * z + y * z + v * w) Lvzxwyw Luw Lxzyzvw 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) Lvz Lxw Lyw Luw (from right to left).
rewrite the current goal using add_SNo_assoc_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw (from right to left).
We will prove v * z + x * w + y * w + u * w < x * z + y * z + v * w + u * w.
Apply SNoLeLt_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) Lvz Lxw Lyw Luw) (SNo_add_SNo_4 (x * z) (u * z) (v * w) (y * w) Lxz Luz Lvw Lyw) (SNo_add_SNo_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw) to the current goal.
We will prove v * 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) Lyw Luw (from left to right).
We will prove v * 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) Lvz Lxw Luw Lyw (from left to right).
We will prove y * 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) Lxz Luz Lvw Lyw (from left to right).
We will prove y * w + v * z + x * w + u * w ≤ y * w + x * z + u * z + v * w.
Apply add_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) Lvz Lxw Luw) (SNo_add_SNo_3 (x * z) (u * z) (v * w) Lxz Luz Lvw) to the current goal.
We will prove v * z + x * w + u * w ≤ x * z + u * z + v * w.
rewrite the current goal using IHyz u (SNoL_SNoS y Hy u Hu) w (SNoL_SNoS z Hz w Hw) (from right to left).
We will prove v * z + (x + u) * w ≤ x * z + u * z + v * w.
rewrite the current goal using add_SNo_assoc (x * z) (u * z) (v * w) Lxz Luz Lvw (from left to right).
We will prove v * z + (x + u) * w ≤ (x * z + u * z) + v * w.
rewrite the current goal using IHy u (SNoL_SNoS y Hy u Hu) (from right to left).
We will prove v * z + (x + u) * w ≤ (x + u) * z + v * w.
Apply mul_SNo_Le (x + u) z v w Lxu Hz Hv1 Hw1 to the current goal.
We will prove v ≤ x + u.
An exact proof term for the current goal is Hvu.
We will prove w ≤ z.
Apply SNoLtLe to the current goal.
We will prove w < z.
An exact proof term for the current goal is Hw3.
We will prove x * z + u * z + v * w + y * w < x * z + y * z + v * w + u * w.
Apply add_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) Luz Lvw Lyw) (SNo_add_SNo_3 (y * z) (v * w) (u * w) Lyz Lvw Luw) to the current goal.
We will prove u * 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) Luz Lvw Lyw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (y * z) (v * w) (u * w) Lyz Lvw Luw (from left to right).
We will prove v * w + u * z + y * w < v * w + y * z + u * w.
Apply add_SNo_Lt2 (v * w) (u * z + y * w) (y * z + u * w) Lvw (SNo_add_SNo (u * z) (y * w) Luz Lyw) (SNo_add_SNo (y * z) (u * w) Lyz Luw) to the current goal.
We will prove u * z + y * w < y * z + u * w.
An exact proof term for the current goal is mul_SNo_Lt y z u w Hy Hz Hu1 Hw1 Hu3 Hw3.
Let v be given.
Assume Hv: v ∈ SNoR (x + y).
Let w be given.
Assume Hw: w ∈ SNoR z.
Assume Hue: u = v * z + (x + y) * w + - v * w.
rewrite the current goal using Hue (from left to right).
We will prove v * z + (x + y) * w + - v * w < x * z + y * z.
Apply SNoR_E (x + y) Lxy v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lxwyw: SNo (x * w + y * w).
An exact proof term for the current goal is SNo_add_SNo (x * w) (y * w) Lxw Lyw.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lvzxwyw: SNo (v * z + x * w + y * w).
An exact proof term for the current goal is SNo_add_SNo_3 (v * z) (x * w) (y * w) Lvz Lxw Lyw.
We prove the intermediate claim Lxzyzvw: SNo (x * z + y * z + v * w).
An exact proof term for the current goal is SNo_add_SNo_3 (x * z) (y * z) (v * w) Lxz Lyz Lvw.
Apply add_SNo_minus_Lt1b3 (v * z) ((x + y) * w) (v * w) (x * z + y * z) Lvz Lxyw Lvw Lxzyz to the current goal.
We will prove v * z + (x + y) * w < (x * z + y * z) + v * w.
rewrite the current goal using IHz w (SNoR_SNoS z Hz w Hw) (from left to right).
We will prove v * z + x * w + y * w < (x * z + y * z) + v * w.
rewrite the current goal using add_SNo_assoc (x * z) (y * z) (v * w) Lxz Lyz Lvw (from right to left).
We will prove v * z + x * w + y * w < x * z + y * z + v * w.
Apply add_SNo_SNoR_interpolate x y Hx Hy v Hv to the current goal.
Assume H1.
Apply H1 to the current goal.
Let u be given.
Assume H1.
Apply H1 to the current goal.
Assume Hu: u ∈ SNoR x.
Assume Hvu: u + y ≤ v.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
We prove the intermediate claim Luw: SNo (u * w).
An exact proof term for the current goal is SNo_mul_SNo u w Hu1 Hw1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu1 Hz.
We prove the intermediate claim Luy: SNo (u + y).
An exact proof term for the current goal is SNo_add_SNo u y Hu1 Hy.
Apply add_SNo_Lt1_cancel (v * z + x * w + y * w) (u * w) (x * z + y * z + v * w) Lvzxwyw Luw Lxzyzvw 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) Lvz Lxw Lyw Luw (from right to left).
rewrite the current goal using add_SNo_assoc_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw (from right to left).
We will prove v * z + x * w + y * w + u * w < x * z + y * z + v * w + u * w.
Apply SNoLeLt_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) Lvz Lxw Lyw Luw) (SNo_add_SNo_4 (u * z) (y * z) (v * w) (x * w) Luz Lyz Lvw Lxw) (SNo_add_SNo_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw) to the current goal.
We will prove v * 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) Lvz Lxw (SNo_add_SNo (y * w) (u * w) Lyw Luw) (from left to right).
We will prove x * 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) Luz Lyz Lvw Lxw (from left to right).
We will prove x * w + v * z + y * w + u * w ≤ x * w + u * z + y * z + v * w.
Apply add_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) Lvz Lyw Luw) (SNo_add_SNo_3 (u * z) (y * z) (v * w) Luz Lyz Lvw) to the current goal.
We will prove v * z + y * w + u * w ≤ u * z + y * z + v * w.
rewrite the current goal using add_SNo_com (y * w) (u * w) Lyw Luw (from left to right).
We will prove v * z + u * w + y * w ≤ u * z + y * z + v * w.
rewrite the current goal using IHxz u (SNoR_SNoS x Hx u Hu) w (SNoR_SNoS z Hz w Hw) (from right to left).
We will prove v * z + (u + y) * w ≤ u * z + y * z + v * w.
rewrite the current goal using add_SNo_assoc (u * z) (y * z) (v * w) Luz Lyz Lvw (from left to right).
We will prove v * z + (u + y) * w ≤ (u * z + y * z) + v * w.
rewrite the current goal using IHx u (SNoR_SNoS x Hx u Hu) (from right to left).
We will prove v * 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) z Luy Hz) Lvw (from left to right).
rewrite the current goal using add_SNo_com (v * z) ((u + y) * w) Lvz (SNo_mul_SNo (u + y) w Luy Hw1) (from left to right).
Apply mul_SNo_Le v w (u + y) z Hv1 Hw1 Luy Hz to the current goal.
We will prove u + y ≤ v.
An exact proof term for the current goal is Hvu.
We will prove z ≤ w.
Apply SNoLtLe to the current goal.
We will prove z < w.
An exact proof term for the current goal is Hw3.
We will prove u * 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) Luz Lyz (SNo_add_SNo (v * w) (x * w) Lvw Lxw) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (x * z) (y * z) (v * w + u * w) Lxz Lyz (SNo_add_SNo (v * w) (u * w) Lvw Luw) (from left to right).
We will prove y * z + u * z + v * w + x * w < y * z + x * z + v * w + u * w.
Apply add_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) Luz Lvw Lxw) (SNo_add_SNo_3 (x * z) (v * w) (u * w) Lxz Lvw Luw) to the current goal.
We will prove u * 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) Luz Lvw Lxw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (x * z) (v * w) (u * w) Lxz Lvw Luw (from left to right).
We will prove v * w + u * z + x * w < v * w + x * z + u * w.
Apply add_SNo_Lt2 (v * w) (u * z + x * w) (x * z + u * w) Lvw (SNo_add_SNo (u * z) (x * w) Luz Lxw) (SNo_add_SNo (x * z) (u * w) Lxz Luw) to the current goal.
We will prove u * z + x * w < x * z + u * w.
rewrite the current goal using add_SNo_com (x * z) (u * w) Lxz Luw (from left to right).
rewrite the current goal using add_SNo_com (u * z) (x * w) Luz Lxw (from left to right).
We will prove x * w + u * z < u * w + x * z.
An exact proof term for the current goal is mul_SNo_Lt u w x z Hu1 Hw1 Hx Hz Hu3 Hw3.
Assume H1.
Apply H1 to the current goal.
Let u be given.
Assume H1.
Apply H1 to the current goal.
Assume Hu: u ∈ SNoR y.
Assume Hvu: x + u ≤ v.
Apply SNoR_E y Hy u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
We prove the intermediate claim Luw: SNo (u * w).
An exact proof term for the current goal is SNo_mul_SNo u w Hu1 Hw1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu1 Hz.
We prove the intermediate claim Lxu: SNo (x + u).
An exact proof term for the current goal is SNo_add_SNo x u Hx Hu1.
Apply add_SNo_Lt1_cancel (v * z + x * w + y * w) (u * w) (x * z + y * z + v * w) Lvzxwyw Luw Lxzyzvw 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) Lvz Lxw Lyw Luw (from right to left).
rewrite the current goal using add_SNo_assoc_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw (from right to left).
We will prove v * z + x * w + y * w + u * w < x * z + y * z + v * w + u * w.
Apply SNoLeLt_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) Lvz Lxw Lyw Luw) (SNo_add_SNo_4 (x * z) (u * z) (v * w) (y * w) Lxz Luz Lvw Lyw) (SNo_add_SNo_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw) to the current goal.
We will prove v * 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) Lyw Luw (from left to right).
We will prove v * 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) Lvz Lxw Luw Lyw (from left to right).
We will prove y * 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) Lxz Luz Lvw Lyw (from left to right).
We will prove y * w + v * z + x * w + u * w ≤ y * w + x * z + u * z + v * w.
Apply add_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) Lvz Lxw Luw) (SNo_add_SNo_3 (x * z) (u * z) (v * w) Lxz Luz Lvw) to the current goal.
We will prove v * z + x * w + u * w ≤ x * z + u * z + v * w.
rewrite the current goal using IHyz u (SNoR_SNoS y Hy u Hu) w (SNoR_SNoS z Hz w Hw) (from right to left).
We will prove v * z + (x + u) * w ≤ x * z + u * z + v * w.
rewrite the current goal using add_SNo_assoc (x * z) (u * z) (v * w) Lxz Luz Lvw (from left to right).
We will prove v * z + (x + u) * w ≤ (x * z + u * z) + v * w.
rewrite the current goal using IHy u (SNoR_SNoS y Hy u Hu) (from right to left).
We will prove v * 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) z Lxu Hz) Lvw (from left to right).
rewrite the current goal using add_SNo_com (v * z) ((x + u) * w) Lvz (SNo_mul_SNo (x + u) w Lxu Hw1) (from left to right).
Apply mul_SNo_Le v w (x + u) z Hv1 Hw1 Lxu Hz to the current goal.
We will prove x + u ≤ v.
An exact proof term for the current goal is Hvu.
We will prove z ≤ w.
Apply SNoLtLe to the current goal.
We will prove z < w.
An exact proof term for the current goal is Hw3.
We will prove x * z + u * z + v * w + y * w < x * z + y * z + v * w + u * w.
Apply add_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) Luz Lvw Lyw) (SNo_add_SNo_3 (y * z) (v * w) (u * w) Lyz Lvw Luw) to the current goal.
We will prove u * 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) Luz Lvw Lyw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (y * z) (v * w) (u * w) Lyz Lvw Luw (from left to right).
We will prove v * w + u * z + y * w < v * w + y * z + u * w.
Apply add_SNo_Lt2 (v * w) (u * z + y * w) (y * z + u * w) Lvw (SNo_add_SNo (u * z) (y * w) Luz Lyw) (SNo_add_SNo (y * z) (u * w) Lyz Luw) to the current goal.
We will prove u * z + y * w < y * z + u * w.
rewrite the current goal using add_SNo_com (y * z) (u * w) Lyz Luw (from left to right).
rewrite the current goal using add_SNo_com (u * z) (y * w) Luz Lyw (from left to right).
We will prove y * w + u * z < u * w + y * z.
An exact proof term for the current goal is mul_SNo_Lt u w y z Hu1 Hw1 Hy Hz Hu3 Hw3.
Let u be given.
Assume Hu: u ∈ R.
rewrite the current goal using LE (from right to left).
We will prove x * z + y * z < u.
Apply HRE u Hu to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL (x + y).
Let w be given.
Assume Hw: w ∈ SNoR z.
Assume Hue: u = v * z + (x + y) * w + - v * w.
rewrite the current goal using Hue (from left to right).
We will prove x * z + y * z < v * z + (x + y) * w + - v * w.
Apply SNoL_E (x + y) Lxy v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lxwyw: SNo (x * w + y * w).
An exact proof term for the current goal is SNo_add_SNo (x * w) (y * w) Lxw Lyw.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lvzxwyw: SNo (v * z + x * w + y * w).
An exact proof term for the current goal is SNo_add_SNo_3 (v * z) (x * w) (y * w) Lvz Lxw Lyw.
We prove the intermediate claim Lxzyzvw: SNo (x * z + y * z + v * w).
An exact proof term for the current goal is SNo_add_SNo_3 (x * z) (y * z) (v * w) Lxz Lyz Lvw.
We will prove x * z + y * z < v * z + (x + y) * w + - v * w.
Apply add_SNo_minus_Lt2b3 (v * z) ((x + y) * w) (v * w) (x * z + y * z) Lvz Lxyw Lvw Lxzyz to the current goal.
We will prove (x * z + y * z) + v * w < v * z + (x + y) * w.
rewrite the current goal using IHz w (SNoR_SNoS z Hz w Hw) (from left to right).
We will prove (x * z + y * z) + v * w < v * z + x * w + y * w.
rewrite the current goal using add_SNo_assoc (x * z) (y * z) (v * w) Lxz Lyz Lvw (from right to left).
We will prove x * z + y * z + v * w < v * z + x * w + y * w.
Apply add_SNo_SNoL_interpolate x y Hx Hy v Hv to the current goal.
Assume H1.
Apply H1 to the current goal.
Let u be given.
Assume H1.
Apply H1 to the current goal.
Assume Hu: u ∈ SNoL x.
Assume Hvu: v ≤ u + y.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
We prove the intermediate claim Luw: SNo (u * w).
An exact proof term for the current goal is SNo_mul_SNo u w Hu1 Hw1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu1 Hz.
We prove the intermediate claim Luy: SNo (u + y).
An exact proof term for the current goal is SNo_add_SNo u y Hu1 Hy.
Apply add_SNo_Lt1_cancel (x * z + y * z + v * w) (u * w) (v * z + x * w + y * w) Lxzyzvw Luw Lvzxwyw 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) Lvz Lxw Lyw Luw (from right to left).
rewrite the current goal using add_SNo_assoc_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw (from right to left).
We will prove x * z + y * z + v * w + u * w < v * z + x * w + y * w + u * w.
Apply SNoLtLe_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) Lxz Lyz Lvw Luw) (SNo_add_SNo_4 (u * z) (y * z) (v * w) (x * w) Luz Lyz Lvw Lxw) (SNo_add_SNo_4 (v * z) (x * w) (y * w) (u * w) Lvz Lxw Lyw Luw) to the current goal.
We will prove x * 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) Luz Lyz (SNo_add_SNo (v * w) (x * w) Lvw Lxw) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (x * z) (y * z) (v * w + u * w) Lxz Lyz (SNo_add_SNo (v * w) (u * w) Lvw Luw) (from left to right).
We will prove y * z + x * z + v * w + u * w < y * z + u * z + v * w + x * w.
Apply add_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) Lxz Lvw Luw) (SNo_add_SNo_3 (u * z) (v * w) (x * w) Luz Lvw Lxw) to the current goal.
We will prove x * 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) Luz Lvw Lxw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (x * z) (v * w) (u * w) Lxz Lvw Luw (from left to right).
We will prove v * w + x * z + u * w < v * w + u * z + x * w.
Apply add_SNo_Lt2 (v * w) (x * z + u * w) (u * z + x * w) Lvw (SNo_add_SNo (x * z) (u * w) Lxz Luw) (SNo_add_SNo (u * z) (x * w) Luz Lxw) to the current goal.
We will prove x * z + u * w < u * z + x * w.
rewrite the current goal using add_SNo_com (x * z) (u * w) Lxz Luw (from left to right).
rewrite the current goal using add_SNo_com (u * z) (x * w) Luz Lxw (from left to right).
An exact proof term for the current goal is mul_SNo_Lt x w u z Hx Hw1 Hu1 Hz Hu3 Hw3.
We will prove u * 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) Lvz Lxw (SNo_add_SNo (y * w) (u * w) Lyw Luw) (from left to right).
We will prove u * 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) Luz Lyz Lvw Lxw (from left to right).
We will prove x * w + u * z + y * z + v * w ≤ x * w + v * z + y * w + u * w.
Apply add_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) Luz Lyz Lvw) (SNo_add_SNo_3 (v * z) (y * w) (u * w) Lvz Lyw Luw) to the current goal.
We will prove u * z + y * z + v * w ≤ v * z + y * w + u * w.
rewrite the current goal using add_SNo_com (y * w) (u * w) Lyw Luw (from left to right).
We will prove u * z + y * z + v * w ≤ v * z + u * w + y * w.
rewrite the current goal using IHxz u (SNoL_SNoS x Hx u Hu) w (SNoR_SNoS z Hz w Hw) (from right to left).
We will prove u * z + y * z + v * w ≤ v * z + (u + y) * w.
rewrite the current goal using add_SNo_assoc (u * z) (y * z) (v * w) Luz Lyz Lvw (from left to right).
We will prove (u * z + y * z) + v * w ≤ v * z + (u + y) * w.
rewrite the current goal using IHx u (SNoL_SNoS x Hx u Hu) (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) z Luy Hz) Lvw (from left to right).
rewrite the current goal using add_SNo_com (v * z) ((u + y) * w) Lvz (SNo_mul_SNo (u + y) w Luy Hw1) (from left to right).
We will prove v * w + (u + y) * z ≤ (u + y) * w + v * z.
Apply mul_SNo_Le (u + y) w v z Luy Hw1 Hv1 Hz to the current goal.
We will prove v ≤ u + y.
An exact proof term for the current goal is Hvu.
We will prove z ≤ w.
Apply SNoLtLe to the current goal.
We will prove z < w.
An exact proof term for the current goal is Hw3.
Assume H1.
Apply H1 to the current goal.
Let u be given.
Assume H1.
Apply H1 to the current goal.
Assume Hu: u ∈ SNoL y.
Assume Hvu: v ≤ x + u.
Apply SNoL_E y Hy u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
We prove the intermediate claim Luw: SNo (u * w).
An exact proof term for the current goal is SNo_mul_SNo u w Hu1 Hw1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu1 Hz.
We prove the intermediate claim Lxu: SNo (x + u).
An exact proof term for the current goal is SNo_add_SNo x u Hx Hu1.
Apply add_SNo_Lt1_cancel (x * z + y * z + v * w) (u * w) (v * z + x * w + y * w) Lxzyzvw Luw Lvzxwyw 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) Lvz Lxw Lyw Luw (from right to left).
rewrite the current goal using add_SNo_assoc_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw (from right to left).
We will prove x * z + y * z + v * w + u * w < v * z + x * w + y * w + u * w.
Apply SNoLtLe_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) Lxz Lyz Lvw Luw) (SNo_add_SNo_4 (x * z) (u * z) (v * w) (y * w) Lxz Luz Lvw Lyw) (SNo_add_SNo_4 (v * z) (x * w) (y * w) (u * w) Lvz Lxw Lyw Luw) to the current goal.
We will prove x * z + y * z + v * w + u * w < x * z + u * z + v * w + y * w.
Apply add_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) Lyz Lvw Luw) (SNo_add_SNo_3 (u * z) (v * w) (y * w) Luz Lvw Lyw) to the current goal.
We will prove y * 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) Luz Lvw Lyw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (y * z) (v * w) (u * w) Lyz Lvw Luw (from left to right).
We will prove v * w + y * z + u * w < v * w + u * z + y * w.
Apply add_SNo_Lt2 (v * w) (y * z + u * w) (u * z + y * w) Lvw (SNo_add_SNo (y * z) (u * w) Lyz Luw) (SNo_add_SNo (u * z) (y * w) Luz Lyw) to the current goal.
We will prove y * z + u * w < u * z + y * w.
rewrite the current goal using add_SNo_com (y * z) (u * w) Lyz Luw (from left to right).
rewrite the current goal using add_SNo_com (u * z) (y * w) Luz Lyw (from left to right).
An exact proof term for the current goal is mul_SNo_Lt y w u z Hy Hw1 Hu1 Hz Hu3 Hw3.
We will prove x * 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) Lyw Luw (from left to right).
We will prove x * 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) Lvz Lxw Luw Lyw (from left to right).
We will prove x * 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) Lxz Luz Lvw Lyw (from left to right).
We will prove y * w + x * z + u * z + v * w ≤ y * w + v * z + x * w + u * w.
Apply add_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) Lxz Luz Lvw) (SNo_add_SNo_3 (v * z) (x * w) (u * w) Lvz Lxw Luw) to the current goal.
We will prove x * z + u * z + v * w ≤ v * z + x * w + u * w.
rewrite the current goal using IHyz u (SNoL_SNoS y Hy u Hu) w (SNoR_SNoS z Hz w Hw) (from right to left).
We will prove x * z + u * z + v * w ≤ v * z + (x + u) * w.
rewrite the current goal using add_SNo_assoc (x * z) (u * z) (v * w) Lxz Luz Lvw (from left to right).
We will prove (x * z + u * z) + v * w ≤ v * z + (x + u) * w.
rewrite the current goal using IHy u (SNoL_SNoS y Hy u Hu) (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) z Lxu Hz) Lvw (from left to right).
rewrite the current goal using add_SNo_com (v * z) ((x + u) * w) Lvz (SNo_mul_SNo (x + u) w Lxu Hw1) (from left to right).
We will prove v * w + (x + u) * z ≤ (x + u) * w + v * z.
Apply mul_SNo_Le (x + u) w v z Lxu Hw1 Hv1 Hz to the current goal.
We will prove v ≤ x + u.
An exact proof term for the current goal is Hvu.
We will prove z ≤ w.
Apply SNoLtLe to the current goal.
We will prove z < w.
An exact proof term for the current goal is Hw3.
Let v be given.
Assume Hv: v ∈ SNoR (x + y).
Let w be given.
Assume Hw: w ∈ SNoL z.
Assume Hue: u = v * z + (x + y) * w + - v * w.
rewrite the current goal using Hue (from left to right).
We will prove x * z + y * z < v * z + (x + y) * w + - v * w.
Apply SNoR_E (x + y) Lxy v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoL_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lxwyw: SNo (x * w + y * w).
An exact proof term for the current goal is SNo_add_SNo (x * w) (y * w) Lxw Lyw.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lvzxwyw: SNo (v * z + x * w + y * w).
An exact proof term for the current goal is SNo_add_SNo_3 (v * z) (x * w) (y * w) Lvz Lxw Lyw.
We prove the intermediate claim Lxzyzvw: SNo (x * z + y * z + v * w).
An exact proof term for the current goal is SNo_add_SNo_3 (x * z) (y * z) (v * w) Lxz Lyz Lvw.
We will prove x * z + y * z < v * z + (x + y) * w + - v * w.
Apply add_SNo_minus_Lt2b3 (v * z) ((x + y) * w) (v * w) (x * z + y * z) Lvz Lxyw Lvw Lxzyz to the current goal.
We will prove (x * z + y * z) + v * w < v * z + (x + y) * w.
rewrite the current goal using IHz w (SNoL_SNoS z Hz w Hw) (from left to right).
We will prove (x * z + y * z) + v * w < v * z + x * w + y * w.
rewrite the current goal using add_SNo_assoc (x * z) (y * z) (v * w) Lxz Lyz Lvw (from right to left).
We will prove x * z + y * z + v * w < v * z + x * w + y * w.
Apply add_SNo_SNoR_interpolate x y Hx Hy v Hv to the current goal.
Assume H1.
Apply H1 to the current goal.
Let u be given.
Assume H1.
Apply H1 to the current goal.
Assume Hu: u ∈ SNoR x.
Assume Hvu: u + y ≤ v.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
We prove the intermediate claim Luw: SNo (u * w).
An exact proof term for the current goal is SNo_mul_SNo u w Hu1 Hw1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu1 Hz.
We prove the intermediate claim Luy: SNo (u + y).
An exact proof term for the current goal is SNo_add_SNo u y Hu1 Hy.
Apply add_SNo_Lt1_cancel (x * z + y * z + v * w) (u * w) (v * z + x * w + y * w) Lxzyzvw Luw Lvzxwyw 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) Lvz Lxw Lyw Luw (from right to left).
rewrite the current goal using add_SNo_assoc_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw (from right to left).
We will prove x * z + y * z + v * w + u * w < v * z + x * w + y * w + u * w.
Apply SNoLtLe_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) Lxz Lyz Lvw Luw) (SNo_add_SNo_4 (u * z) (y * z) (v * w) (x * w) Luz Lyz Lvw Lxw) (SNo_add_SNo_4 (v * z) (x * w) (y * w) (u * w) Lvz Lxw Lyw Luw) to the current goal.
We will prove x * 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) Luz Lyz (SNo_add_SNo (v * w) (x * w) Lvw Lxw) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (x * z) (y * z) (v * w + u * w) Lxz Lyz (SNo_add_SNo (v * w) (u * w) Lvw Luw) (from left to right).
We will prove y * z + x * z + v * w + u * w < y * z + u * z + v * w + x * w.
Apply add_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) Lxz Lvw Luw) (SNo_add_SNo_3 (u * z) (v * w) (x * w) Luz Lvw Lxw) to the current goal.
We will prove x * 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) Luz Lvw Lxw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (x * z) (v * w) (u * w) Lxz Lvw Luw (from left to right).
We will prove v * w + x * z + u * w < v * w + u * z + x * w.
Apply add_SNo_Lt2 (v * w) (x * z + u * w) (u * z + x * w) Lvw (SNo_add_SNo (x * z) (u * w) Lxz Luw) (SNo_add_SNo (u * z) (x * w) Luz Lxw) to the current goal.
We will prove x * z + u * w < u * z + x * w.
An exact proof term for the current goal is mul_SNo_Lt u z x w Hu1 Hz Hx Hw1 Hu3 Hw3.
We will prove u * 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) Lvz Lxw (SNo_add_SNo (y * w) (u * w) Lyw Luw) (from left to right).
We will prove u * 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) Luz Lyz Lvw Lxw (from left to right).
We will prove x * w + u * z + y * z + v * w ≤ x * w + v * z + y * w + u * w.
Apply add_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) Luz Lyz Lvw) (SNo_add_SNo_3 (v * z) (y * w) (u * w) Lvz Lyw Luw) to the current goal.
We will prove u * z + y * z + v * w ≤ v * z + y * w + u * w.
rewrite the current goal using add_SNo_com (y * w) (u * w) Lyw Luw (from left to right).
We will prove u * z + y * z + v * w ≤ v * z + u * w + y * w.
rewrite the current goal using IHxz u (SNoR_SNoS x Hx u Hu) w (SNoL_SNoS z Hz w Hw) (from right to left).
We will prove u * z + y * z + v * w ≤ v * z + (u + y) * w.
rewrite the current goal using add_SNo_assoc (u * z) (y * z) (v * w) Luz Lyz Lvw (from left to right).
We will prove (u * z + y * z) + v * w ≤ v * z + (u + y) * w.
rewrite the current goal using IHx u (SNoR_SNoS x Hx u Hu) (from right to left).
We will prove (u + y) * z + v * w ≤ v * z + (u + y) * w.
Apply mul_SNo_Le v z (u + y) w Hv1 Hz Luy Hw1 to the current goal.
We will prove u + y ≤ v.
An exact proof term for the current goal is Hvu.
We will prove w ≤ z.
Apply SNoLtLe to the current goal.
We will prove w < z.
An exact proof term for the current goal is Hw3.
Assume H1.
Apply H1 to the current goal.
Let u be given.
Assume H1.
Apply H1 to the current goal.
Assume Hu: u ∈ SNoR y.
Assume Hvu: x + u ≤ v.
Apply SNoR_E y Hy u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
We prove the intermediate claim Luw: SNo (u * w).
An exact proof term for the current goal is SNo_mul_SNo u w Hu1 Hw1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu1 Hz.
We prove the intermediate claim Lxu: SNo (x + u).
An exact proof term for the current goal is SNo_add_SNo x u Hx Hu1.
Apply add_SNo_Lt1_cancel (x * z + y * z + v * w) (u * w) (v * z + x * w + y * w) Lxzyzvw Luw Lvzxwyw 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) Lvz Lxw Lyw Luw (from right to left).
rewrite the current goal using add_SNo_assoc_4 (x * z) (y * z) (v * w) (u * w) Lxz Lyz Lvw Luw (from right to left).
We will prove x * z + y * z + v * w + u * w < v * z + x * w + y * w + u * w.
Apply SNoLtLe_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) Lxz Lyz Lvw Luw) (SNo_add_SNo_4 (x * z) (u * z) (v * w) (y * w) Lxz Luz Lvw Lyw) (SNo_add_SNo_4 (v * z) (x * w) (y * w) (u * w) Lvz Lxw Lyw Luw) to the current goal.
We will prove x * z + y * z + v * w + u * w < x * z + u * z + v * w + y * w.
Apply add_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) Lyz Lvw Luw) (SNo_add_SNo_3 (u * z) (v * w) (y * w) Luz Lvw Lyw) to the current goal.
We will prove y * 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) Luz Lvw Lyw (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (y * z) (v * w) (u * w) Lyz Lvw Luw (from left to right).
We will prove v * w + y * z + u * w < v * w + u * z + y * w.
Apply add_SNo_Lt2 (v * w) (y * z + u * w) (u * z + y * w) Lvw (SNo_add_SNo (y * z) (u * w) Lyz Luw) (SNo_add_SNo (u * z) (y * w) Luz Lyw) to the current goal.
We will prove y * z + u * w < u * z + y * w.
An exact proof term for the current goal is mul_SNo_Lt u z y w Hu1 Hz Hy Hw1 Hu3 Hw3.
We will prove x * 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) Lyw Luw (from left to right).
We will prove x * 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) Lvz Lxw Luw Lyw (from left to right).
We will prove x * 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) Lxz Luz Lvw Lyw (from left to right).
We will prove y * w + x * z + u * z + v * w ≤ y * w + v * z + x * w + u * w.
Apply add_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) Lxz Luz Lvw) (SNo_add_SNo_3 (v * z) (x * w) (u * w) Lvz Lxw Luw) to the current goal.
We will prove x * z + u * z + v * w ≤ v * z + x * w + u * w.
rewrite the current goal using IHyz u (SNoR_SNoS y Hy u Hu) w (SNoL_SNoS z Hz w Hw) (from right to left).
We will prove x * z + u * z + v * w ≤ v * z + (x + u) * w.
rewrite the current goal using add_SNo_assoc (x * z) (u * z) (v * w) Lxz Luz Lvw (from left to right).
We will prove (x * z + u * z) + v * w ≤ v * z + (x + u) * w.
rewrite the current goal using IHy u (SNoR_SNoS y Hy u Hu) (from right to left).
We will prove (x + u) * z + v * w ≤ v * z + (x + u) * w.
Apply mul_SNo_Le v z (x + u) w Hv1 Hz Lxu Hw1 to the current goal.
We will prove x + u ≤ v.
An exact proof term for the current goal is Hvu.
We will prove w ≤ z.
Apply SNoLtLe to the current goal.
We will prove w < z.
An exact proof term for the current goal is Hw3.
Let u' be given.
Assume Hu': u' ∈ L1 ∪ L2.
rewrite the current goal using HE (from right to left).
We will prove u' < (x + y) * z.
Apply binunionE L1 L2 u' Hu' to the current goal.
Assume Hu': u' ∈ L1.
Apply ReplE_impred (SNoL (x * z)) (λw ⇒ w + y * z) u' Hu' to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL (x * z).
Assume Hu'u: u' = u + y * z.
rewrite the current goal using Hu'u (from left to right).
We will prove u + y * z < (x + y) * z.
Apply SNoL_E (x * z) Lxz u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
Apply mul_SNo_SNoL_interpolate_impred x z Hx Hz u Hu to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Let w be given.
Assume Hw: w ∈ SNoL z.
Assume Hvw: u + v * w ≤ v * z + x * w.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoL_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lvy: SNo (v + y).
An exact proof term for the current goal is SNo_add_SNo v y Hv1 Hy.
We prove the intermediate claim Luvw: SNo (u + v * w).
An exact proof term for the current goal is SNo_add_SNo u (v * w) Hu1 Lvw.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Luyz: SNo (u + y * z).
An exact proof term for the current goal is SNo_add_SNo u (y * z) Hu1 Lyz.
We prove the intermediate claim Lvwyw: SNo (v * w + y * w).
An exact proof term for the current goal is SNo_add_SNo (v * w) (y * w) Lvw Lyw.
We prove the intermediate claim Lvzxw: SNo (v * z + x * w).
An exact proof term for the current goal is SNo_add_SNo (v * z) (x * w) Lvz Lxw.
We will prove u + y * z < (x + y) * z.
Apply add_SNo_Lt1_cancel (u + y * z) (v * w + y * w) ((x + y) * z) Luyz Lvwyw Lxyz 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_mid u (y * z) (v * w) (y * w) Hu1 Lyz Lvw Lyw (from left to right).
We will prove (u + v * w) + y * z + y * w < (x + y) * z + v * w + y * w.
Apply SNoLeLt_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) Luvw Lyz Lyw) (SNo_add_SNo_4 (v * z) (y * z) (x * w) (y * w) Lvz Lyz Lxw Lyw) (SNo_add_SNo_3 ((x + y) * z) (v * w) (y * w) Lxyz Lvw Lyw) 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) Lvz Lyz (SNo_add_SNo (x * w) (y * w) Lxw Lyw) (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) Lvz Lyz Lxw Lyw (from left to right).
We will prove (u + v * w) + y * z + y * w ≤ (v * z + x * w) + y * z + y * w.
Apply add_SNo_Le1 (u + v * w) (y * z + y * w) (v * z + x * w) Luvw (SNo_add_SNo (y * z) (y * w) Lyz Lyw) (SNo_add_SNo (v * z) (x * w) Lvz Lxw) to the current goal.
We will prove u + v * w ≤ v * z + x * w.
An exact proof term for the current goal is Hvw.
We will prove v * z + y * z + x * w + y * w < (x + y) * z + v * w + y * w.
rewrite the current goal using IHz w (SNoL_SNoS z Hz w Hw) (from right to left).
We will prove v * z + y * z + (x + y) * w < (x + y) * z + v * w + y * w.
rewrite the current goal using IHxz v (SNoL_SNoS x Hx v Hv) w (SNoL_SNoS z Hz w Hw) (from right to left).
We will prove v * 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) Lvz Lyz Lxyw (from left to right).
rewrite the current goal using IHx v (SNoL_SNoS x Hx v Hv) (from right to left).
We will prove (v + y) * z + (x + y) * w < (x + y) * z + (v + y) * w.
Apply mul_SNo_Lt (x + y) z (v + y) w Lxy Hz Lvy Hw1 to the current goal.
We will prove v + y < x + y.
Apply add_SNo_Lt1 v y x Hv1 Hy Hx to the current goal.
An exact proof term for the current goal is Hv3.
We will prove w < z.
An exact proof term for the current goal is Hw3.
Let v be given.
Assume Hv: v ∈ SNoR x.
Let w be given.
Assume Hw: w ∈ SNoR z.
Assume Hvw: u + v * w ≤ v * z + x * w.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lvy: SNo (v + y).
An exact proof term for the current goal is SNo_add_SNo v y Hv1 Hy.
We prove the intermediate claim Luvw: SNo (u + v * w).
An exact proof term for the current goal is SNo_add_SNo u (v * w) Hu1 Lvw.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Luyz: SNo (u + y * z).
An exact proof term for the current goal is SNo_add_SNo u (y * z) Hu1 Lyz.
We prove the intermediate claim Lvwyw: SNo (v * w + y * w).
An exact proof term for the current goal is SNo_add_SNo (v * w) (y * w) Lvw Lyw.
We will prove u + y * z < (x + y) * z.
Apply add_SNo_Lt1_cancel (u + y * z) (v * w + y * w) ((x + y) * z) Luyz Lvwyw Lxyz 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_mid u (y * z) (v * w) (y * w) Hu1 Lyz Lvw Lyw (from left to right).
We will prove (u + v * w) + y * z + y * w < (x + y) * z + v * w + y * w.
Apply SNoLeLt_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) Luvw Lyz Lyw) (SNo_add_SNo_4 (v * z) (y * z) (x * w) (y * w) Lvz Lyz Lxw Lyw) (SNo_add_SNo_3 ((x + y) * z) (v * w) (y * w) Lxyz Lvw Lyw) 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) Lvz Lyz (SNo_add_SNo (x * w) (y * w) Lxw Lyw) (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) Lvz Lyz Lxw Lyw (from left to right).
We will prove (u + v * w) + y * z + y * w ≤ (v * z + x * w) + y * z + y * w.
Apply add_SNo_Le1 (u + v * w) (y * z + y * w) (v * z + x * w) Luvw (SNo_add_SNo (y * z) (y * w) Lyz Lyw) (SNo_add_SNo (v * z) (x * w) Lvz Lxw) to the current goal.
We will prove u + v * w ≤ v * z + x * w.
An exact proof term for the current goal is Hvw.
We will prove v * z + y * z + x * w + y * w < (x + y) * z + v * w + y * w.
rewrite the current goal using IHz w (SNoR_SNoS z Hz w Hw) (from right to left).
We will prove v * z + y * z + (x + y) * w < (x + y) * z + v * w + y * w.
rewrite the current goal using IHxz v (SNoR_SNoS x Hx v Hv) w (SNoR_SNoS z Hz w Hw) (from right to left).
We will prove v * 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) Lvz Lyz Lxyw (from left to right).
rewrite the current goal using IHx v (SNoR_SNoS x Hx v Hv) (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) z Lvy Hz) 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) w Lvy Hw1) (from left to right).
Apply mul_SNo_Lt (v + y) w (x + y) z Lvy Hw1 Lxy Hz to the current goal.
We will prove x + y < v + y.
Apply add_SNo_Lt1 x y v Hx Hy Hv1 to the current goal.
An exact proof term for the current goal is Hv3.
We will prove z < w.
An exact proof term for the current goal is Hw3.
Assume Hu': u' ∈ L2.
Apply ReplE_impred (SNoL (y * z)) (λw ⇒ x * z + w) u' Hu' to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL (y * z).
Assume Hu'u: u' = x * z + u.
rewrite the current goal using Hu'u (from left to right).
We will prove x * z + u < (x + y) * z.
Apply SNoL_E (y * z) Lyz u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
rewrite the current goal using add_SNo_com (x * z) u Lxz Hu1 (from left to right).
We will prove u + x * z < (x + y) * z.
Apply mul_SNo_SNoL_interpolate_impred y z Hy Hz u Hu to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL y.
Let w be given.
Assume Hw: w ∈ SNoL z.
Assume Hvw: u + v * w ≤ v * z + y * w.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoL_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lxv: SNo (x + v).
An exact proof term for the current goal is SNo_add_SNo x v Hx Hv1.
We prove the intermediate claim Luvw: SNo (u + v * w).
An exact proof term for the current goal is SNo_add_SNo u (v * w) Hu1 Lvw.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Luxz: SNo (u + x * z).
An exact proof term for the current goal is SNo_add_SNo u (x * z) Hu1 Lxz.
We prove the intermediate claim Lvwxw: SNo (v * w + x * w).
An exact proof term for the current goal is SNo_add_SNo (v * w) (x * w) Lvw Lxw.
We will prove u + x * z < (x + y) * z.
Apply add_SNo_Lt1_cancel (u + x * z) (v * w + x * w) ((x + y) * z) Luxz Lvwxw Lxyz 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_mid u (x * z) (v * w) (x * w) Hu1 Lxz Lvw Lxw (from left to right).
We will prove (u + v * w) + x * z + x * w < (x + y) * z + v * w + x * w.
Apply SNoLeLt_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) Luvw Lxz Lxw) (SNo_add_SNo_4 (v * z) (x * z) (x * w) (y * w) Lvz Lxz Lxw Lyw) (SNo_add_SNo_3 ((x + y) * z) (v * w) (x * w) Lxyz Lvw Lxw) 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) Lvz Lxz (SNo_add_SNo (x * w) (y * w) Lxw Lyw) (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) Lxw Lyw (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) Lvz Lxz Lyw Lxw (from left to right).
We will prove (u + v * w) + x * z + x * w ≤ (v * z + y * w) + x * z + x * w.
Apply add_SNo_Le1 (u + v * w) (x * z + x * w) (v * z + y * w) Luvw (SNo_add_SNo (x * z) (x * w) Lxz Lxw) (SNo_add_SNo (v * z) (y * w) Lvz Lyw) to the current goal.
We will prove u + v * w ≤ v * z + y * w.
An exact proof term for the current goal is Hvw.
We will prove v * z + x * z + x * w + y * w < (x + y) * z + v * w + x * w.
rewrite the current goal using IHz w (SNoL_SNoS z Hz w Hw) (from right to left).
We will prove v * 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) Lvw Lxw (from left to right).
rewrite the current goal using IHyz v (SNoL_SNoS y Hy v Hv) w (SNoL_SNoS z Hz w Hw) (from right to left).
We will prove v * 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) Lvz Lxz Lxyw (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) Lvz Lxz (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 IHy v (SNoL_SNoS y Hy v Hv) (from right to left).
We will prove (x + v) * z + (x + y) * w < (x + y) * z + (x + v) * w.
Apply mul_SNo_Lt (x + y) z (x + v) w Lxy Hz Lxv Hw1 to the current goal.
We will prove x + v < x + y.
Apply add_SNo_Lt2 x v y Hx Hv1 Hy to the current goal.
An exact proof term for the current goal is Hv3.
We will prove w < z.
An exact proof term for the current goal is Hw3.
Let v be given.
Assume Hv: v ∈ SNoR y.
Let w be given.
Assume Hw: w ∈ SNoR z.
Assume Hvw: u + v * w ≤ v * z + y * w.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lxv: SNo (x + v).
An exact proof term for the current goal is SNo_add_SNo x v Hx Hv1.
We prove the intermediate claim Luvw: SNo (u + v * w).
An exact proof term for the current goal is SNo_add_SNo u (v * w) Hu1 Lvw.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Luxz: SNo (u + x * z).
An exact proof term for the current goal is SNo_add_SNo u (x * z) Hu1 Lxz.
We prove the intermediate claim Lvwxw: SNo (v * w + x * w).
An exact proof term for the current goal is SNo_add_SNo (v * w) (x * w) Lvw Lxw.
We prove the intermediate claim Lvzxw: SNo (v * z + x * w).
An exact proof term for the current goal is SNo_add_SNo (v * z) (x * w) Lvz Lxw.
We will prove u + x * z < (x + y) * z.
Apply add_SNo_Lt1_cancel (u + x * z) (v * w + x * w) ((x + y) * z) Luxz Lvwxw Lxyz 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_mid u (x * z) (v * w) (x * w) Hu1 Lxz Lvw Lxw (from left to right).
We will prove (u + v * w) + x * z + x * w < (x + y) * z + v * w + x * w.
Apply SNoLeLt_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) Luvw Lxz Lxw) (SNo_add_SNo_4 (v * z) (x * z) (x * w) (y * w) Lvz Lxz Lxw Lyw) (SNo_add_SNo_3 ((x + y) * z) (v * w) (x * w) Lxyz Lvw Lxw) 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) Lvz Lxz (SNo_add_SNo (x * w) (y * w) Lxw Lyw) (from left to right).
rewrite the current goal using add_SNo_com (y * w) (x * w) Lyw Lxw (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) Lvz Lxz Lyw Lxw (from left to right).
We will prove (u + v * w) + x * z + x * w ≤ (v * z + y * w) + x * z + x * w.
Apply add_SNo_Le1 (u + v * w) (x * z + x * w) (v * z + y * w) Luvw (SNo_add_SNo (x * z) (x * w) Lxz Lxw) (SNo_add_SNo (v * z) (y * w) Lvz Lyw) to the current goal.
We will prove u + v * w ≤ v * z + y * w.
An exact proof term for the current goal is Hvw.
We will prove v * z + x * z + x * w + y * w < (x + y) * z + v * w + x * w.
rewrite the current goal using IHz w (SNoR_SNoS z Hz w Hw) (from right to left).
We will prove v * 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) Lvw Lxw (from left to right).
We will prove v * z + x * z + (x + y) * w < (x + y) * z + x * w + v * w.
rewrite the current goal using IHyz v (SNoR_SNoS y Hy v Hv) w (SNoR_SNoS z Hz w Hw) (from right to left).
We will prove v * 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) Lvz Lxz Lxyw (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) Lvz Lxz (from left to right).
rewrite the current goal using IHy v (SNoR_SNoS y Hy v Hv) (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) z Lxv Hz) 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) w Lxv Hw1) (from left to right).
We will prove (x + y) * w + (x + v) * z < (x + v) * w + (x + y) * z.
Apply mul_SNo_Lt (x + v) w (x + y) z Lxv Hw1 Lxy Hz to the current goal.
We will prove x + y < x + v.
Apply add_SNo_Lt2 x y v Hx Hy Hv1 to the current goal.
An exact proof term for the current goal is Hv3.
We will prove z < w.
An exact proof term for the current goal is Hw3.
Let u' be given.
Assume Hu': u' ∈ R1 ∪ R2.
rewrite the current goal using HE (from right to left).
We will prove (x + y) * z < u'.
Apply binunionE R1 R2 u' Hu' to the current goal.
Assume Hu': u' ∈ R1.
Apply ReplE_impred (SNoR (x * z)) (λw ⇒ w + y * z) u' Hu' to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR (x * z).
Assume Hu'u: u' = u + y * z.
rewrite the current goal using Hu'u (from left to right).
We will prove (x + y) * z < u + y * z.
Apply SNoR_E (x * z) Lxz u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
Apply mul_SNo_SNoR_interpolate_impred x z Hx Hz u Hu to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Let w be given.
Assume Hw: w ∈ SNoR z.
Assume Hvw: v * z + x * w ≤ u + v * w.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lvy: SNo (v + y).
An exact proof term for the current goal is SNo_add_SNo v y Hv1 Hy.
We prove the intermediate claim Luvw: SNo (u + v * w).
An exact proof term for the current goal is SNo_add_SNo u (v * w) Hu1 Lvw.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Luyz: SNo (u + y * z).
An exact proof term for the current goal is SNo_add_SNo u (y * z) Hu1 Lyz.
We prove the intermediate claim Lvwyw: SNo (v * w + y * w).
An exact proof term for the current goal is SNo_add_SNo (v * w) (y * w) Lvw Lyw.
We prove the intermediate claim Lvzxw: SNo (v * z + x * w).
An exact proof term for the current goal is SNo_add_SNo (v * z) (x * w) Lvz Lxw.
We will prove (x + y) * z < u + y * z.
Apply add_SNo_Lt1_cancel ((x + y) * z) (v * w + y * w) (u + y * z) Lxyz Lvwyw Luyz 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_mid u (y * z) (v * w) (y * w) Hu1 Lyz Lvw Lyw (from left to right).
We will prove (x + y) * z + v * w + y * w < (u + v * w) + y * z + y * w.
Apply SNoLtLe_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) Lxyz Lvw Lyw) (SNo_add_SNo_4 (v * z) (y * z) (x * w) (y * w) Lvz Lyz Lxw Lyw) (SNo_add_SNo_3 (u + v * w) (y * z) (y * w) Luvw Lyz Lyw) 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 IHz w (SNoR_SNoS z Hz w Hw) (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 IHxz v (SNoL_SNoS x Hx v Hv) w (SNoR_SNoS z Hz w Hw) (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) Lvz Lyz Lxyw (from left to right).
rewrite the current goal using IHx v (SNoL_SNoS x Hx v Hv) (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) w Lvy Hw1) (from left to right).
rewrite the current goal using add_SNo_com ((v + y) * z) ((x + y) * w) (SNo_mul_SNo (v + y) z Lvy Hz) Lxyw (from left to right).
We will prove (v + y) * w + (x + y) * z < (x + y) * w + (v + y) * z.
Apply mul_SNo_Lt (x + y) w (v + y) z Lxy Hw1 Lvy Hz to the current goal.
We will prove v + y < x + y.
Apply add_SNo_Lt1 v y x Hv1 Hy Hx to the current goal.
An exact proof term for the current goal is Hv3.
We will prove z < w.
An exact proof term for the current goal is Hw3.
We will prove v * z + y * z + x * w + y * w ≤ (u + v * w) + y * z + y * w.
rewrite the current goal using add_SNo_assoc (v * z) (y * z) (x * w + y * w) Lvz Lyz (SNo_add_SNo (x * w) (y * w) Lxw Lyw) (from left to right).
We will prove (v * z + y * z) + x * w + y * w ≤ (u + v * w) + y * z + y * w.
rewrite the current goal using add_SNo_com_4_inner_mid (v * z) (y * z) (x * w) (y * w) Lvz Lyz Lxw Lyw (from left to right).
We will prove (v * z + x * w) + y * z + y * w ≤ (u + v * w) + y * z + y * w.
Apply add_SNo_Le1 (v * z + x * w) (y * z + y * w) (u + v * w) (SNo_add_SNo (v * z) (x * w) Lvz Lxw) (SNo_add_SNo (y * z) (y * w) Lyz Lyw) Luvw to the current goal.
We will prove v * z + x * w ≤ u + v * w.
An exact proof term for the current goal is Hvw.
Let v be given.
Assume Hv: v ∈ SNoR x.
Let w be given.
Assume Hw: w ∈ SNoL z.
Assume Hvw: v * z + x * w ≤ u + v * w.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoL_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lvy: SNo (v + y).
An exact proof term for the current goal is SNo_add_SNo v y Hv1 Hy.
We prove the intermediate claim Luvw: SNo (u + v * w).
An exact proof term for the current goal is SNo_add_SNo u (v * w) Hu1 Lvw.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Luyz: SNo (u + y * z).
An exact proof term for the current goal is SNo_add_SNo u (y * z) Hu1 Lyz.
We prove the intermediate claim Lvwyw: SNo (v * w + y * w).
An exact proof term for the current goal is SNo_add_SNo (v * w) (y * w) Lvw Lyw.
We will prove (x + y) * z < u + y * z.
Apply add_SNo_Lt1_cancel ((x + y) * z) (v * w + y * w) (u + y * z) Lxyz Lvwyw Luyz 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_mid u (y * z) (v * w) (y * w) Hu1 Lyz Lvw Lyw (from left to right).
We will prove (x + y) * z + v * w + y * w < (u + v * w) + y * z + y * w.
Apply SNoLtLe_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) Lxyz Lvw Lyw) (SNo_add_SNo_4 (v * z) (y * z) (x * w) (y * w) Lvz Lyz Lxw Lyw) (SNo_add_SNo_3 (u + v * w) (y * z) (y * w) Luvw Lyz Lyw) 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 IHz w (SNoL_SNoS z Hz w Hw) (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 IHxz v (SNoR_SNoS x Hx v Hv) w (SNoL_SNoS z Hz w Hw) (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) Lvz Lyz Lxyw (from left to right).
rewrite the current goal using IHx v (SNoR_SNoS x Hx v Hv) (from right to left).
We will prove (x + y) * z + (v + y) * w < (v + y) * z + (x + y) * w.
Apply mul_SNo_Lt (v + y) z (x + y) w Lvy Hz Lxy Hw1 to the current goal.
We will prove x + y < v + y.
Apply add_SNo_Lt1 x y v Hx Hy Hv1 to the current goal.
An exact proof term for the current goal is Hv3.
We will prove w < z.
An exact proof term for the current goal is Hw3.
We will prove v * z + y * z + x * w + y * w ≤ (u + v * w) + y * z + y * w.
rewrite the current goal using add_SNo_assoc (v * z) (y * z) (x * w + y * w) Lvz Lyz (SNo_add_SNo (x * w) (y * w) Lxw Lyw) (from left to right).
We will prove (v * z + y * z) + x * w + y * w ≤ (u + v * w) + y * z + y * w.
rewrite the current goal using add_SNo_com_4_inner_mid (v * z) (y * z) (x * w) (y * w) Lvz Lyz Lxw Lyw (from left to right).
We will prove (v * z + x * w) + y * z + y * w ≤ (u + v * w) + y * z + y * w.
Apply add_SNo_Le1 (v * z + x * w) (y * z + y * w) (u + v * w) (SNo_add_SNo (v * z) (x * w) Lvz Lxw) (SNo_add_SNo (y * z) (y * w) Lyz Lyw) Luvw to the current goal.
We will prove v * z + x * w ≤ u + v * w.
An exact proof term for the current goal is Hvw.
Assume Hu': u' ∈ R2.
Apply ReplE_impred (SNoR (y * z)) (λw ⇒ x * z + w) u' Hu' to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR (y * z).
Assume Hu'u: u' = x * z + u.
rewrite the current goal using Hu'u (from left to right).
We will prove (x + y) * z < x * z + u.
Apply SNoR_E (y * z) Lyz u Hu to the current goal.
Assume Hu1 Hu2 Hu3.
rewrite the current goal using add_SNo_com (x * z) u Lxz Hu1 (from left to right).
We will prove (x + y) * z < u + x * z.
Apply mul_SNo_SNoR_interpolate_impred y z Hy Hz u Hu to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL y.
Let w be given.
Assume Hw: w ∈ SNoR z.
Assume Hvw: v * z + y * w ≤ u + v * w.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lxv: SNo (x + v).
An exact proof term for the current goal is SNo_add_SNo x v Hx Hv1.
We prove the intermediate claim Luvw: SNo (u + v * w).
An exact proof term for the current goal is SNo_add_SNo u (v * w) Hu1 Lvw.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Luxz: SNo (u + x * z).
An exact proof term for the current goal is SNo_add_SNo u (x * z) Hu1 Lxz.
We prove the intermediate claim Lvwxw: SNo (v * w + x * w).
An exact proof term for the current goal is SNo_add_SNo (v * w) (x * w) Lvw Lxw.
We will prove (x + y) * z < u + x * z.
Apply add_SNo_Lt1_cancel ((x + y) * z) (v * w + x * w) (u + x * z) Lxyz Lvwxw Luxz 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_mid u (x * z) (v * w) (x * w) Hu1 Lxz Lvw Lxw (from left to right).
We will prove (x + y) * z + v * w + x * w < (u + v * w) + x * z + x * w.
Apply SNoLtLe_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) Lxyz Lvw Lxw) (SNo_add_SNo_4 (v * z) (x * z) (x * w) (y * w) Lvz Lxz Lxw Lyw) (SNo_add_SNo_3 (u + v * w) (x * z) (x * w) Luvw Lxz Lxw) 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 IHz w (SNoR_SNoS z Hz w Hw) (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) Lvw Lxw (from left to right).
rewrite the current goal using IHyz v (SNoL_SNoS y Hy v Hv) w (SNoR_SNoS z Hz w Hw) (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) Lvz Lxz Lxyw (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) Lvz Lxz (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 IHy v (SNoL_SNoS y Hy v Hv) (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) w Lxv Hw1) (from left to right).
rewrite the current goal using add_SNo_com ((x + v) * z) ((x + y) * w) (SNo_mul_SNo (x + v) z Lxv Hz) Lxyw (from left to right).
We will prove (x + v) * w + (x + y) * z < (x + y) * w + (x + v) * z.
Apply mul_SNo_Lt (x + y) w (x + v) z Lxy Hw1 Lxv Hz to the current goal.
We will prove x + v < x + y.
Apply add_SNo_Lt2 x v y Hx Hv1 Hy to the current goal.
An exact proof term for the current goal is Hv3.
We will prove z < w.
An exact proof term for the current goal is Hw3.
We will prove v * z + x * z + x * w + y * w ≤ (u + v * w) + x * z + x * w.
rewrite the current goal using add_SNo_assoc (v * z) (x * z) (x * w + y * w) Lvz Lxz (SNo_add_SNo (x * w) (y * w) Lxw Lyw) (from left to right).
We will prove (v * z + x * z) + x * w + y * w ≤ (u + v * w) + x * z + x * w.
rewrite the current goal using add_SNo_com (x * w) (y * w) Lxw Lyw (from left to right).
We will prove (v * z + x * z) + y * w + x * w ≤ (u + v * w) + x * z + x * w.
rewrite the current goal using add_SNo_com_4_inner_mid (v * z) (x * z) (y * w) (x * w) Lvz Lxz Lyw Lxw (from left to right).
We will prove (v * z + y * w) + x * z + x * w ≤ (u + v * w) + x * z + x * w.
Apply add_SNo_Le1 (v * z + y * w) (x * z + x * w) (u + v * w) (SNo_add_SNo (v * z) (y * w) Lvz Lyw) (SNo_add_SNo (x * z) (x * w) Lxz Lxw) Luvw to the current goal.
We will prove v * z + y * w ≤ u + v * w.
An exact proof term for the current goal is Hvw.
Let v be given.
Assume Hv: v ∈ SNoR y.
Let w be given.
Assume Hw: w ∈ SNoL z.
Assume Hvw: v * z + y * w ≤ u + v * w.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv1 Hv2 Hv3.
Apply SNoL_E z Hz w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Lvw: SNo (v * w).
An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.
We prove the intermediate claim Lxv: SNo (x + v).
An exact proof term for the current goal is SNo_add_SNo x v Hx Hv1.
We prove the intermediate claim Luvw: SNo (u + v * w).
An exact proof term for the current goal is SNo_add_SNo u (v * w) Hu1 Lvw.
We prove the intermediate claim Lxyw: SNo ((x + y) * w).
An exact proof term for the current goal is SNo_mul_SNo (x + y) w Lxy Hw1.
We prove the intermediate claim Lvz: SNo (v * z).
An exact proof term for the current goal is SNo_mul_SNo v z Hv1 Hz.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
We prove the intermediate claim Lyw: SNo (y * w).
An exact proof term for the current goal is SNo_mul_SNo y w Hy Hw1.
We prove the intermediate claim Luxz: SNo (u + x * z).
An exact proof term for the current goal is SNo_add_SNo u (x * z) Hu1 Lxz.
We prove the intermediate claim Lvwxw: SNo (v * w + x * w).
An exact proof term for the current goal is SNo_add_SNo (v * w) (x * w) Lvw Lxw.
We prove the intermediate claim Lvzxw: SNo (v * z + x * w).
An exact proof term for the current goal is SNo_add_SNo (v * z) (x * w) Lvz Lxw.
We will prove (x + y) * z < u + x * z.
Apply add_SNo_Lt1_cancel ((x + y) * z) (v * w + x * w) (u + x * z) Lxyz Lvwxw Luxz 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_mid u (x * z) (v * w) (x * w) Hu1 Lxz Lvw Lxw (from left to right).
We will prove (x + y) * z + v * w + x * w < (u + v * w) + x * z + x * w.
Apply SNoLtLe_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) Lxyz Lvw Lxw) (SNo_add_SNo_4 (v * z) (x * z) (x * w) (y * w) Lvz Lxz Lxw Lyw) (SNo_add_SNo_3 (u + v * w) (x * z) (x * w) Luvw Lxz Lxw) 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 IHz w (SNoL_SNoS z Hz w Hw) (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) Lvw Lxw (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 IHyz v (SNoR_SNoS y Hy v Hv) w (SNoL_SNoS z Hz w Hw) (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) Lvz Lxz Lxyw (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) Lvz Lxz (from left to right).
rewrite the current goal using IHy v (SNoR_SNoS y Hy v Hv) (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) z Lxv Hz) 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) w Lxv Hw1) (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) w Lxv Hw1) 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) z Lxv Hz) (from left to right).
We will prove (x + y) * z + (x + v) * w < (x + v) * z + (x + y) * w.
Apply mul_SNo_Lt (x + v) z (x + y) w Lxv Hz Lxy Hw1 to the current goal.
We will prove x + y < x + v.
Apply add_SNo_Lt2 x y v Hx Hy Hv1 to the current goal.
An exact proof term for the current goal is Hv3.
We will prove w < z.
An exact proof term for the current goal is Hw3.
We will prove v * z + x * z + x * w + y * w ≤ (u + v * w) + x * z + x * w.
rewrite the current goal using add_SNo_assoc (v * z) (x * z) (x * w + y * w) Lvz Lxz (SNo_add_SNo (x * w) (y * w) Lxw Lyw) (from left to right).
rewrite the current goal using add_SNo_com (y * w) (x * w) Lyw Lxw (from right to left).
We will prove (v * z + x * z) + y * w + x * w ≤ (u + v * w) + x * z + x * w.
rewrite the current goal using add_SNo_com_4_inner_mid (v * z) (x * z) (y * w) (x * w) Lvz Lxz Lyw Lxw (from left to right).
We will prove (v * z + y * w) + x * z + x * w ≤ (u + v * w) + x * z + x * w.
Apply add_SNo_Le1 (v * z + y * w) (x * z + x * w) (u + v * w) (SNo_add_SNo (v * z) (y * w) Lvz Lyw) (SNo_add_SNo (x * z) (x * w) Lxz Lxw) Luvw to the current goal.
We will prove v * z + y * w ≤ u + v * w.
An exact proof term for the current goal is Hvw.
∎