Let v be given.

Assume Hv.

Let w be given.

Assume Hw.

Let w1 be given.

Assume Hw1.

Let w2 be given.

Assume Hw2.

Assume Hue H1 H2.

Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) v Hv to the current goal.

Assume Hv1 Hv2 Hv3 Hv4.

Apply SNoS_E2 (SNoLev y) (SNoLev_ordinal y Hy) w1 Hw1 to the current goal.

Assume Hw11 Hw12 Hw13 Hw14.

Apply SNoS_E2 (SNoLev z) (SNoLev_ordinal z Hz) w2 Hw2 to the current goal.

Assume Hw21 Hw22 Hw23 Hw24.

We prove the intermediate claim Lvyz: SNo (v * (y * z)).

An exact proof term for the current goal is SNo_M v (y * z) Hv3 Lyz.

We prove the intermediate claim Lxw: SNo (x * w).

An exact proof term for the current goal is SNo_M x w Hx Hw.

We prove the intermediate claim Lxw1: SNo (x * w1).

An exact proof term for the current goal is SNo_M x w1 Hx Hw13.

We prove the intermediate claim Lvw: SNo (v * w).

An exact proof term for the current goal is SNo_M v w Hv3 Hw.

We prove the intermediate claim Lvw1: SNo (v * w1).

An exact proof term for the current goal is SNo_M v w1 Hv3 Hw13.

We prove the intermediate claim Lvy: SNo (v * y).

An exact proof term for the current goal is SNo_M v y Hv3 Hy.

We prove the intermediate claim Lw1z: SNo (w1 * z).

An exact proof term for the current goal is SNo_M w1 z Hw13 Hz.

We prove the intermediate claim Lyw2: SNo (y * w2).

An exact proof term for the current goal is SNo_M y w2 Hy Hw23.

We prove the intermediate claim Lvw1z: SNo (v * (w1 * z)).

An exact proof term for the current goal is SNo_M v (w1 * z) Hv3 Lw1z.

We prove the intermediate claim Lvyw2: SNo (v * (y * w2)).

An exact proof term for the current goal is SNo_M v (y * w2) Hv3 Lyw2.

We prove the intermediate claim Lw1w2: SNo (w1 * w2).

An exact proof term for the current goal is SNo_M w1 w2 Hw13 Hw23.

We prove the intermediate claim Lxw1w2: SNo (x * (w1 * w2)).

An exact proof term for the current goal is SNo_M x (w1 * w2) Hx Lw1w2.

We prove the intermediate claim Lxw1z: SNo (x * (w1 * z)).

An exact proof term for the current goal is SNo_M x (w1 * z) Hx Lw1z.

We prove the intermediate claim Lxyw2: SNo (x * (y * w2)).

An exact proof term for the current goal is SNo_M x (y * w2) Hx Lyw2.

We prove the intermediate claim Lvyzxw: SNo (v * (y * z) + x * w).

An exact proof term for the current goal is SNo_add_SNo (v * (y * z)) (x * w) Lvyz Lxw.

We prove the intermediate claim Lxyzvw: SNo ((x * y) * z + v * w).

An exact proof term for the current goal is SNo_add_SNo ((x * y) * z) (v * w) Lxyz2 Lvw.

We prove the intermediate claim Lvw1w2: SNo (v * (w1 * w2)).

An exact proof term for the current goal is SNo_M v (w1 * w2) Hv3 Lw1w2.

We prove the intermediate claim Lww1w2: SNo (w + w1 * w2).

An exact proof term for the current goal is SNo_add_SNo w (w1 * w2) Hw Lw1w2.

We prove the intermediate claim Lvww1w2: SNo (v * (w + w1 * w2)).

An exact proof term for the current goal is SNo_M v (w + w1 * w2) Hv3 Lww1w2.

We prove the intermediate claim Lvw1zyw2: SNo (v * (w1 * z + y * w2)).

An exact proof term for the current goal is SNo_M v (w1 * z + y * w2) Hv3 (SNo_add_SNo (w1 * z) (y * w2) Lw1z Lyw2).

We prove the intermediate claim Lvwvw1w2: SNo (v * w + v * (w1 * w2)).

An exact proof term for the current goal is SNo_add_SNo (v * w) (v * (w1 * w2)) Lvw Lvw1w2.

We prove the intermediate claim Lvyzxw1zxyw2vwvw1w2: 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)) Lvyz Lxw1z Lxyw2 Lvwvw1w2.

We prove the intermediate claim Lvw1zvyw2xw1w2: 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)) Lvw1z Lvyw2 Lxw1w2.

rewrite the current goal using Hue (from left to right).

Apply add_SNo_minus_Lt2b3 (v * (y * z)) (x * w) (v * w) ((x * y) * z) Lvyz Lxw Lvw Lxyz2 to the current goal.

We will prove (x * y) * z + v * w < v * (y * z) + x * w.

Apply add_SNo_Lt1_cancel ((x * y) * z + v * w) (v * (w1 * z) + v * (y * w2) + x * (w1 * w2)) (v * (y * z) + x * w) Lxyzvw Lvw1zvyw2xw1w2 Lvyzxw 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).

Apply SNoLtLe_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.

Apply SNo_add_SNo to the current goal.

An exact proof term for the current goal is Lxyzvw.

An exact proof term for the current goal is Lvw1zvyw2xw1w2.

An exact proof term for the current goal is Lvyzxw1zxyw2vwvw1w2.

Apply SNo_add_SNo 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) Lxyz2 Lvw (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)) Lvw Lxyz2 Lvw1zvyw2xw1w2 (from right to left).

We will prove v * 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)) Lvyz Lxw1z Lxyw2 Lvw Lvw1w2 (from left to right).

We will prove v * 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).

Apply add_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)) Lxyz2 Lvw1z Lvyw2 Lxw1w2) (SNo_add_SNo_4 (v * (w1 * w2)) (v * (y * z)) (x * (w1 * z)) (x * (y * w2)) Lvw1w2 Lvyz Lxw1z Lxyw2) 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)) Lxyz2 Lvw1z (SNo_add_SNo (v * (y * w2)) (x * (w1 * w2)) Lvyw2 Lxw1w2) (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 IHxz v Hv w2 Hw2 (from left to right).

rewrite the current goal using IHyz w1 Hw1 w2 Hw2 (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) w2 Lvy Lxw1 Hw23 (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 IHxy v Hv w1 Hw1 (from left to right).

rewrite the current goal using DR (x * y) (v * w1) z Lxy Lvw1 Hz (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)) Lvyz Lxw1z Lxyw2 Lvw1w2 (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)) Lvyz Lxw1z (SNo_add_SNo (x * (y * w2)) (v * (w1 * w2)) Lxyw2 Lvw1w2) (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 IHx v Hv (from left to right).

rewrite the current goal using IHy w1 Hw1 (from left to right).

rewrite the current goal using IHz w2 Hw2 (from left to right).

rewrite the current goal using IHxyz v Hv w1 Hw1 w2 Hw2 (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) z Lvy Lxw1 Hz (from right to left).

rewrite the current goal using DR (x * y) (v * w1) w2 Lxy Lvw1 Hw23 (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 prove 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).

rewrite the current goal using add_SNo_assoc (v * (y * z)) (x * w) (v * (w1 * z) + v * (y * w2) + x * (w1 * w2)) Lvyz Lxw Lvw1zvyw2xw1w2 (from right to left).

We will prove 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).

Apply add_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)) Lxw1z Lxyw2 Lvw Lvw1w2) (SNo_add_SNo (x * w) (v * (w1 * z) + v * (y * w2) + x * (w1 * w2)) Lxw Lvw1zvyw2xw1w2) to the current goal.

We will prove x * (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)) Lvw1z Lvyw2 Lxw1w2 (from left to right).

rewrite the current goal using DL v (w1 * z) (y * w2) Hv3 Lw1z Lyw2 (from right to left).

We will prove x * (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)) Lxw Lvw1zyw2 Lxw1w2 (from left to right).

We will prove x * (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 DL x w (w1 * w2) Hx Hw Lw1w2 (from right to left).

We will prove x * (w1 * z) + x * (y * w2) + v * w + v * (w1 * w2) ≤ v * (w1 * z + y * w2) + x * (w + w1 * w2).

rewrite the current goal using DL v w (w1 * w2) Hv3 Hw Lw1w2 (from right to left).

We will prove x * (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)) Lxw1z Lxyw2 Lvww1w2 (from left to right).

rewrite the current goal using DL x (w1 * z) (y * w2) Hx Lw1z Lyw2 (from right to left).

We will prove x * (w1 * z + y * w2) + v * (w + w1 * w2) ≤ v * (w1 * z + y * w2) + x * (w + w1 * w2).

An exact proof term for the current goal is H1.

Let v be given.

Assume Hv: v ∈ SNoL x.

Let w be given.

Assume Hw: w ∈ SNoR (y * z).

Assume Hue: u = v * (y * z) + x * w + - v * w.

Apply SNoL_E x Hx v Hv to the current goal.

Assume Hv1 Hv2 Hv3.

We prove the intermediate claim Lw: SNo w.

Apply SNoR_E (y * z) Lyz w Hw to the current goal.

Assume H _ _.

An exact proof term for the current goal is H.

We prove the intermediate claim Lvw: SNo (v * w).

An exact proof term for the current goal is SNo_M v w Hv1 Lw.

We prove the intermediate claim Lvy: SNo (v * y).

An exact proof term for the current goal is SNo_M v y Hv1 Hy.

Apply IR y z Hy Hz w Hw to the current goal.

Let w1 be given.

Assume Hw1: w1 ∈ SNoL y.

Let w2 be given.

Assume Hw2: w2 ∈ SNoR z.

Assume Hwl: w1 * z + y * w2 ≤ w + w1 * w2.

Apply SNoL_E y Hy w1 Hw1 to the current goal.

Assume Hw11 Hw12 Hw13.

Apply SNoR_E z Hz w2 Hw2 to the current goal.

Assume Hw21 Hw22 Hw23.

We prove the intermediate claim Lxw1: SNo (x * w1).

An exact proof term for the current goal is SNo_M x w1 Hx Hw11.

We prove the intermediate claim Lw1z: SNo (w1 * z).

An exact proof term for the current goal is SNo_M w1 z Hw11 Hz.

We prove the intermediate claim Lyw2: SNo (y * w2).

An exact proof term for the current goal is SNo_M y w2 Hy Hw21.

We prove the intermediate claim Lw1zyw2: SNo (w1 * z + y * w2).

An exact proof term for the current goal is SNo_add_SNo (w1 * z) (y * w2) Lw1z Lyw2.

We prove the intermediate claim Lw1w2: SNo (w1 * w2).

An exact proof term for the current goal is SNo_M w1 w2 Hw11 Hw21.

We prove the intermediate claim Lww1w2: SNo (w + w1 * w2).

An exact proof term for the current goal is SNo_add_SNo w (w1 * w2) Lw Lw1w2.

We prove the intermediate claim Lxww1w2: SNo (x * (w + w1 * w2)).

An exact proof term for the current goal is SNo_M x (w + w1 * w2) Hx Lww1w2.

We prove the intermediate claim Lvww1w2: SNo (v * (w + w1 * w2)).

An exact proof term for the current goal is SNo_M v (w + w1 * w2) Hv1 Lww1w2.

We prove the intermediate claim Lvw1w2: SNo (v * (w1 * w2)).

An exact proof term for the current goal is SNo_M v (w1 * w2) Hv1 Lw1w2.

We prove the intermediate claim Lvw1zyw2: SNo (v * (w1 * z + y * w2)).

An exact proof term for the current goal is SNo_M v (w1 * z + y * w2) Hv1 Lw1zyw2.

We prove the intermediate claim Lvwvw1w2: SNo (v * w + v * (w1 * w2)).

An exact proof term for the current goal is SNo_add_SNo (v * w) (v * (w1 * w2)) Lvw Lvw1w2.

We prove the intermediate claim Lxw1zyw2: SNo (x * (w1 * z + y * w2)).

An exact proof term for the current goal is SNo_M x (w1 * z + y * w2) Hx Lw1zyw2.

We prove the intermediate claim Lxyvw1: SNo (x * y + v * w1).

An exact proof term for the current goal is SNo_add_SNo (x * y) (v * w1) Lxy (SNo_M v w1 Hv1 Hw11).

We prove the intermediate claim Lvyxw1: SNo (v * y + x * w1).

An exact proof term for the current goal is SNo_add_SNo (v * y) (x * w1) Lvy Lxw1.

We prove the intermediate claim Lxyvw1z: SNo ((x * y + v * w1) * z).

An exact proof term for the current goal is SNo_M (x * y + v * w1) z Lxyvw1 Hz.

We prove the intermediate claim Lvyxw1z: SNo ((v * y + x * w1) * z).

An exact proof term for the current goal is SNo_M (v * y + x * w1) z Lvyxw1 Hz.

We prove the intermediate claim Lxyvw1: SNo (x * y + v * w1).

An exact proof term for the current goal is SNo_add_SNo (x * y) (v * w1) Lxy (SNo_M v w1 Hv1 Hw11).

We prove the intermediate claim Lxyvw1w2: SNo ((x * y + v * w1) * w2).

An exact proof term for the current goal is SNo_M (x * y + v * w1) w2 Lxyvw1 Hw21.

We prove the intermediate claim Lvyxw1w2: SNo ((v * y + x * w1) * w2).

An exact proof term for the current goal is SNo_M (v * y + x * w1) w2 Lvyxw1 Hw21.

Apply L2 v (SNoL_SNoS x Hx v Hv) w Lw w1 (SNoL_SNoS y Hy w1 Hw1) w2 (SNoR_SNoS z Hz w2 Hw2) Hue to the current goal.

We will prove x * (w1 * z + y * w2) + v * (w + w1 * w2) ≤ v * (w1 * z + y * w2) + x * (w + w1 * w2).

rewrite the current goal using add_SNo_com (v * (w1 * z + y * w2)) (x * (w + w1 * w2)) Lvw1zyw2 Lxww1w2 (from left to right).

rewrite the current goal using add_SNo_com (x * (w1 * z + y * w2)) (v * (w + w1 * w2)) Lxw1zyw2 Lvww1w2 (from left to right).

We will prove v * (w + w1 * w2) + x * (w1 * z + y * w2) ≤ x * (w + w1 * w2) + v * (w1 * z + y * w2).

Apply M_Le x (w + w1 * w2) v (w1 * z + y * w2) Hx Lww1w2 Hv1 Lw1zyw2 to the current goal.

We will prove v ≤ x.

Apply SNoLtLe to the current goal.

An exact proof term for the current goal is Hv3.

An exact proof term for the current goal is Hwl.

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) Lvyxw1z Lxyvw1w2 (from left to right).

rewrite the current goal using add_SNo_com ((x * y + v * w1) * z) ((v * y + x * w1) * w2) Lxyvw1z Lvyxw1w2 (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.

Apply M_Lt (x * y + v * w1) w2 (v * y + x * w1) z (SNo_add_SNo (x * y) (v * w1) Lxy (SNo_M v w1 Hv1 Hw11)) Hw21 (SNo_add_SNo (v * y) (x * w1) (SNo_M v y Hv1 Hy) (SNo_M x w1 Hx Hw11)) Hz to the current goal.

We will prove v * y + x * w1 < x * y + v * w1.

Apply M_Lt x y v w1 Hx Hy Hv1 Hw11 to the current goal.

We will prove v < x.

An exact proof term for the current goal is Hv3.

We will prove w1 < y.

An exact proof term for the current goal is Hw13.

We will prove z < w2.

An exact proof term for the current goal is Hw23.

Let w1 be given.

Assume Hw1: w1 ∈ SNoR y.

Let w2 be given.

Assume Hw2: w2 ∈ SNoL z.

Assume Hwl: w1 * z + y * w2 ≤ w + w1 * w2.

Apply SNoR_E y Hy w1 Hw1 to the current goal.

Assume Hw11 Hw12 Hw13.

Apply SNoL_E z Hz w2 Hw2 to the current goal.

Assume Hw21 Hw22 Hw23.

We prove the intermediate claim Lvy: SNo (v * y).

An exact proof term for the current goal is SNo_M v y Hv1 Hy.

We prove the intermediate claim Lvw1: SNo (v * w1).

An exact proof term for the current goal is SNo_M v w1 Hv1 Hw11.