Let x, y, u and v be given.
Assume Hx Hy Hu Hv Hux Hvy.
Apply mul_SNo_prop_1 x Hx y Hy to the current goal.
Assume Hxy: SNo (x * y).
Assume Hxy1: ∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v.
Assume Hxy2: ∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v.
Assume Hxy3: ∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v.
Assume Hxy4: ∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v.
Apply mul_SNo_prop_1 u Hu y Hy to the current goal.
Assume Huy: SNo (u * y).
Assume Huy1: ∀x ∈ SNoL u, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v.
Assume Huy2: ∀x ∈ SNoR u, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v.
Assume Huy3: ∀x ∈ SNoL u, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v.
Assume Huy4: ∀x ∈ SNoR u, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v.
Apply mul_SNo_prop_1 x Hx v Hv to the current goal.
Assume Hxv: SNo (x * v).
Assume Hxv1: ∀u ∈ SNoL x, ∀y ∈ SNoL v, u * v + x * y < x * v + u * y.
Assume Hxv2: ∀u ∈ SNoR x, ∀y ∈ SNoR v, u * v + x * y < x * v + u * y.
Assume Hxv3: ∀u ∈ SNoL x, ∀y ∈ SNoR v, x * v + u * y < u * v + x * y.
Assume Hxv4: ∀u ∈ SNoR x, ∀y ∈ SNoL v, x * v + u * y < u * v + x * y.
Apply mul_SNo_prop_1 u Hu v Hv to the current goal.
Assume Huv: SNo (u * v).
Assume Huv1: ∀x ∈ SNoL u, ∀y ∈ SNoL v, x * v + u * y < u * v + x * y.
Assume Huv2: ∀x ∈ SNoR u, ∀y ∈ SNoR v, x * v + u * y < u * v + x * y.
Assume Huv3: ∀x ∈ SNoL u, ∀y ∈ SNoR v, u * v + x * y < x * v + u * y.
Assume Huv4: ∀x ∈ SNoR u, ∀y ∈ SNoL v, u * v + x * y < x * v + u * y.
We prove the intermediate claim Luyxv: SNo (u * y + x * v).
An exact proof term for the current goal is SNo_add_SNo (u * y) (x * v) Huy Hxv.
We prove the intermediate claim Lxyuv: SNo (x * y + u * v).
An exact proof term for the current goal is SNo_add_SNo (x * y) (u * v) Hxy Huv.
Apply SNoLtE u x Hu Hx Hux to the current goal.
Let w be given.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev u ∩ SNoLev x.
Assume Hw3: SNoEq_ (SNoLev w) w u.
Assume Hw4: SNoEq_ (SNoLev w) w x.
Assume Hw5: u < w.
Assume Hw6: w < x.
Assume Hw7: SNoLev w ∉ u.
Assume Hw8: SNoLev w ∈ x.
Apply binintersectE (SNoLev u) (SNoLev x) (SNoLev w) Hw2 to the current goal.
Assume Hw2a Hw2b.
We prove the intermediate claim Lwx: w ∈ SNoL x.
An exact proof term for the current goal is SNoL_I x Hx w Hw1 Hw2b Hw6.
We prove the intermediate claim Lwu: w ∈ SNoR u.
An exact proof term for the current goal is SNoR_I u Hu w Hw1 Hw2a Hw5.
We prove the intermediate claim Lwy: SNo (w * y).
An exact proof term for the current goal is SNo_mul_SNo w y Hw1 Hy.
We prove the intermediate claim Lwv: SNo (w * v).
An exact proof term for the current goal is SNo_mul_SNo w v Hw1 Hv.
We prove the intermediate claim Lwyxv: SNo (w * y + x * v).
An exact proof term for the current goal is SNo_add_SNo (w * y) (x * v) Lwy Hxv.
We prove the intermediate claim Lwyuv: SNo (w * y + u * v).
An exact proof term for the current goal is SNo_add_SNo (w * y) (u * v) Lwy Huv.
We prove the intermediate claim Lxywv: SNo (x * y + w * v).
An exact proof term for the current goal is SNo_add_SNo (x * y) (w * v) Hxy Lwv.
We prove the intermediate claim Luywv: SNo (u * y + w * v).
An exact proof term for the current goal is SNo_add_SNo (u * y) (w * v) Huy Lwv.
We prove the intermediate claim Luvwy: SNo (u * v + w * y).
An exact proof term for the current goal is SNo_add_SNo (u * v) (w * y) Huv Lwy.
We prove the intermediate claim Lwvxy: SNo (w * v + x * y).
An exact proof term for the current goal is SNo_add_SNo (w * v) (x * y) Lwv Hxy.
We prove the intermediate claim Lxvwy: SNo (x * v + w * y).
An exact proof term for the current goal is SNo_add_SNo (x * v) (w * y) Hxv Lwy.
We prove the intermediate claim Lwvuy: SNo (w * v + u * y).
An exact proof term for the current goal is SNo_add_SNo (w * v) (u * y) Lwv Huy.
Apply SNoLtE v y Hv Hy Hvy to the current goal.
Let z be given.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev v ∩ SNoLev y.
Assume Hz3: SNoEq_ (SNoLev z) z v.
Assume Hz4: SNoEq_ (SNoLev z) z y.
Assume Hz5: v < z.
Assume Hz6: z < y.
Assume Hz7: SNoLev z ∉ v.
Assume Hz8: SNoLev z ∈ y.
Apply binintersectE (SNoLev v) (SNoLev y) (SNoLev z) Hz2 to the current goal.
Assume Hz2a Hz2b.
We prove the intermediate claim Lzy: z ∈ SNoL y.
An exact proof term for the current goal is SNoL_I y Hy z Hz1 Hz2b Hz6.
We prove the intermediate claim Lzv: z ∈ SNoR v.
An exact proof term for the current goal is SNoR_I v Hv z Hz1 Hz2a Hz5.
We prove the intermediate claim Lxz: SNo (x * z).
An exact proof term for the current goal is SNo_mul_SNo x z Hx Hz1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu Hz1.
We prove the intermediate claim Lwz: SNo (w * z).
An exact proof term for the current goal is SNo_mul_SNo w z Hw1 Hz1.
We prove the intermediate claim L1: w * y + x * z < x * y + w * z.
An exact proof term for the current goal is Hxy1 w Lwx z Lzy.
We prove the intermediate claim L2: w * v + u * z < u * v + w * z.
An exact proof term for the current goal is Huv2 w Lwu z Lzv.
We prove the intermediate claim L3: x * v + w * z < w * v + x * z.
An exact proof term for the current goal is Hxv3 w Lwx z Lzv.
We prove the intermediate claim L4: u * y + w * z < w * y + u * z.
An exact proof term for the current goal is Huy4 w Lwu z Lzy.
We prove the intermediate claim Lwzwz: SNo (w * z + w * z).
An exact proof term for the current goal is SNo_add_SNo (w * z) (w * z) Lwz Lwz.
Apply add_SNo_Lt1_cancel (u * y + x * v) (w * z + w * z) (x * y + u * v) Luyxv Lwzwz Lxyuv to the current goal.
We will prove (u * y + x * v) + (w * z + w * z) < (x * y + u * v) + (w * z + w * z).
We prove the intermediate claim Lwyuz: SNo (w * y + u * z).
An exact proof term for the current goal is SNo_add_SNo (w * y) (u * z) Lwy Luz.
We prove the intermediate claim Lwvxz: SNo (w * v + x * z).
An exact proof term for the current goal is SNo_add_SNo (w * v) (x * z) Lwv Lxz.
We prove the intermediate claim Luywz: SNo (u * y + w * z).
An exact proof term for the current goal is SNo_add_SNo (u * y) (w * z) Huy Lwz.
We prove the intermediate claim Lxvwz: SNo (x * v + w * z).
An exact proof term for the current goal is SNo_add_SNo (x * v) (w * z) Hxv Lwz.
We prove the intermediate claim Lwvuz: SNo (w * v + u * z).
An exact proof term for the current goal is SNo_add_SNo (w * v) (u * z) Lwv Luz.
We prove the intermediate claim Lxyxz: SNo (x * y + x * z).
An exact proof term for the current goal is SNo_add_SNo (x * y) (x * z) Hxy Lxz.
We prove the intermediate claim Lwyxz: SNo (w * y + x * z).
An exact proof term for the current goal is SNo_add_SNo (w * y) (x * z) Lwy Lxz.
We prove the intermediate claim Lxywz: SNo (x * y + w * z).
An exact proof term for the current goal is SNo_add_SNo (x * y) (w * z) Hxy Lwz.
We prove the intermediate claim Luvwz: SNo (u * v + w * z).
An exact proof term for the current goal is SNo_add_SNo (u * v) (w * z) Huv Lwz.
Apply SNoLt_tra ((u * y + x * v) + (w * z + w * z)) ((w * y + u * z) + (w * v + x * z)) ((x * y + u * v) + (w * z + w * z)) (SNo_add_SNo (u * y + x * v) (w * z + w * z) Luyxv Lwzwz) (SNo_add_SNo (w * y + u * z) (w * v + x * z) Lwyuz Lwvxz) (SNo_add_SNo (x * y + u * v) (w * z + w * z) Lxyuv Lwzwz) to the current goal.
We will prove (u * y + x * v) + (w * z + w * z) < (w * y + u * z) + (w * v + x * z).
rewrite the current goal using add_SNo_com_4_inner_mid (u * y) (x * v) (w * z) (w * z) Huy Hxv Lwz Lwz (from left to right).
We will prove (u * y + w * z) + (x * v + w * z) < (w * y + u * z) + (w * v + x * z).
Apply add_SNo_Lt3 (u * y + w * z) (x * v + w * z) (w * y + u * z) (w * v + x * z) Luywz Lxvwz Lwyuz Lwvxz to the current goal.
We will prove u * y + w * z < w * y + u * z.
An exact proof term for the current goal is L4.
We will prove x * v + w * z < w * v + x * z.
An exact proof term for the current goal is L3.
We will prove (w * y + u * z) + (w * v + x * z) < (x * y + u * v) + (w * z + w * z).
rewrite the current goal using add_SNo_com_4_inner_mid (x * y) (u * v) (w * z) (w * z) Hxy Huv Lwz Lwz (from left to right).
We will prove (w * y + u * z) + (w * v + x * z) < (x * y + w * z) + (u * v + w * z).
rewrite the current goal using add_SNo_com (w * y) (u * z) Lwy Luz (from left to right).
rewrite the current goal using add_SNo_com_4_inner_mid (u * z) (w * y) (w * v) (x * z) Luz Lwy Lwv Lxz (from left to right).
rewrite the current goal using add_SNo_com (w * v) (u * z) Lwv Luz (from right to left).
We will prove (w * v + u * z) + (w * y + x * z) < (x * y + w * z) + (u * v + w * z).
rewrite the current goal using add_SNo_com (w * v + u * z) (w * y + x * z) Lwvuz Lwyxz (from left to right).
We will prove (w * y + x * z) + (w * v + u * z) < (x * y + w * z) + (u * v + w * z).
Apply add_SNo_Lt3 (w * y + x * z) (w * v + u * z) (x * y + w * z) (u * v + w * z) Lwyxz Lwvuz Lxywz Luvwz to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.
Assume H4: SNoLev v ∈ SNoLev y.
Assume H5: SNoEq_ (SNoLev v) v y.
Assume H6: SNoLev v ∈ y.
We prove the intermediate claim Lvy: v ∈ SNoL y.
An exact proof term for the current goal is SNoL_I y Hy v Hv H4 Hvy.
We prove the intermediate claim L1: w * y + x * v < x * y + w * v.
An exact proof term for the current goal is Hxy1 w Lwx v Lvy.
We prove the intermediate claim L2: u * y + w * v < w * y + u * v.
An exact proof term for the current goal is Huy4 w Lwu v Lvy.
We will prove u * y + x * v < x * y + u * v.
Apply add_SNo_Lt2_cancel (w * y) (u * y + x * v) (x * y + u * v) Lwy Luyxv Lxyuv to the current goal.
We will prove w * y + u * y + x * v < w * y + x * y + u * v.
Apply SNoLt_tra (w * y + u * y + x * v) (u * y + w * v + x * y) (w * y + x * y + u * v) (SNo_add_SNo (w * y) (u * y + x * v) Lwy Luyxv) (SNo_add_SNo (u * y) (w * v + x * y) Huy (SNo_add_SNo (w * v) (x * y) Lwv Hxy)) (SNo_add_SNo (w * y) (x * y + u * v) Lwy Lxyuv) to the current goal.
We will prove w * y + u * y + x * v < u * y + w * v + x * y.
rewrite the current goal using add_SNo_com_3_0_1 (w * y) (u * y) (x * v) Lwy Huy Hxv (from left to right).
We will prove u * y + w * y + x * v < u * y + w * v + x * y.
rewrite the current goal using add_SNo_com (w * v) (x * y) Lwv Hxy (from left to right).
An exact proof term for the current goal is add_SNo_Lt2 (u * y) (w * y + x * v) (x * y + w * v) Huy Lwyxv Lxywv L1.
We will prove u * y + w * v + x * y < w * y + x * y + u * v.
rewrite the current goal using add_SNo_assoc (u * y) (w * v) (x * y) Huy Lwv Hxy (from left to right).
We will prove (u * y + w * v) + x * y < w * y + x * y + u * v.
rewrite the current goal using add_SNo_com (x * y) (u * v) Hxy Huv (from left to right).
We will prove (u * y + w * v) + x * y < w * y + u * v + x * y.
rewrite the current goal using add_SNo_assoc (w * y) (u * v) (x * y) Lwy Huv Hxy (from left to right).
We will prove (u * y + w * v) + x * y < (w * y + u * v) + x * y.
An exact proof term for the current goal is add_SNo_Lt1 (u * y + w * v) (x * y) (w * y + u * v) Luywv Hxy Lwyuv L2.
Assume H4: SNoLev y ∈ SNoLev v.
Assume H5: SNoEq_ (SNoLev y) v y.
Assume H6: SNoLev y ∉ v.
We prove the intermediate claim Lyv: y ∈ SNoR v.
An exact proof term for the current goal is SNoR_I v Hv y Hy H4 Hvy.
We prove the intermediate claim L1: x * v + w * y < w * v + x * y.
An exact proof term for the current goal is Hxv3 w Lwx y Lyv.
We prove the intermediate claim L2: w * v + u * y < u * v + w * y.
An exact proof term for the current goal is Huv2 w Lwu y Lyv.
We will prove u * y + x * v < x * y + u * v.
Apply add_SNo_Lt2_cancel (w * y) (u * y + x * v) (x * y + u * v) Lwy Luyxv Lxyuv to the current goal.
We will prove w * y + u * y + x * v < w * y + x * y + u * v.
Apply SNoLt_tra (w * y + u * y + x * v) (u * y + w * v + x * y) (w * y + x * y + u * v) (SNo_add_SNo (w * y) (u * y + x * v) Lwy Luyxv) (SNo_add_SNo (u * y) (w * v + x * y) Huy (SNo_add_SNo (w * v) (x * y) Lwv Hxy)) (SNo_add_SNo (w * y) (x * y + u * v) Lwy Lxyuv) to the current goal.
We will prove w * y + u * y + x * v < u * y + w * v + x * y.
rewrite the current goal using add_SNo_rotate_3_1 (u * y) (x * v) (w * y) Huy Hxv Lwy (from right to left).
We will prove u * y + x * v + w * y < u * y + w * v + x * y.
An exact proof term for the current goal is add_SNo_Lt2 (u * y) (x * v + w * y) (w * v + x * y) Huy Lxvwy Lwvxy L1.
We will prove u * y + w * v + x * y < w * y + x * y + u * v.
rewrite the current goal using add_SNo_rotate_3_1 (w * y) (x * y) (u * v) Lwy Hxy Huv (from left to right).
We will prove u * y + w * v + x * y < u * v + w * y + x * y.
rewrite the current goal using add_SNo_assoc (u * y) (w * v) (x * y) Huy Lwv Hxy (from left to right).
rewrite the current goal using add_SNo_assoc (u * v) (w * y) (x * y) Huv Lwy Hxy (from left to right).
We will prove (u * y + w * v) + x * y < (u * v + w * y) + x * y.
rewrite the current goal using add_SNo_com (u * y) (w * v) Huy Lwv (from left to right).
We will prove (w * v + u * y) + x * y < (u * v + w * y) + x * y.
Apply add_SNo_Lt1 (w * v + u * y) (x * y) (u * v + w * y) Lwvuy Hxy Luvwy L2 to the current goal.
Assume H1: SNoLev u ∈ SNoLev x.
Assume H2: SNoEq_ (SNoLev u) u x.
Assume H3: SNoLev u ∈ x.
We prove the intermediate claim Lux: u ∈ SNoL x.
An exact proof term for the current goal is SNoL_I x Hx u Hu H1 Hux.
Apply SNoLtE v y Hv Hy Hvy to the current goal.
Let z be given.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev v ∩ SNoLev y.
Assume Hz3: SNoEq_ (SNoLev z) z v.
Assume Hz4: SNoEq_ (SNoLev z) z y.
Assume Hz5: v < z.
Assume Hz6: z < y.
Assume Hz7: SNoLev z ∉ v.
Assume Hz8: SNoLev z ∈ y.
Apply binintersectE (SNoLev v) (SNoLev y) (SNoLev z) Hz2 to the current goal.
Assume Hz2a Hz2b.
We prove the intermediate claim Lzy: z ∈ SNoL y.
An exact proof term for the current goal is SNoL_I y Hy z Hz1 Hz2b Hz6.
We prove the intermediate claim Lzv: z ∈ SNoR v.
An exact proof term for the current goal is SNoR_I v Hv z Hz1 Hz2a Hz5.
We prove the intermediate claim Lxz: SNo (x * z).
An exact proof term for the current goal is SNo_mul_SNo x z Hx Hz1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu Hz1.
We prove the intermediate claim Luyxz: SNo (u * y + x * z).
An exact proof term for the current goal is SNo_add_SNo (u * y) (x * z) Huy Lxz.
We prove the intermediate claim Luvxz: SNo (u * v + x * z).
An exact proof term for the current goal is SNo_add_SNo (u * v) (x * z) Huv Lxz.
We prove the intermediate claim Lxyuz: SNo (x * y + u * z).
An exact proof term for the current goal is SNo_add_SNo (x * y) (u * z) Hxy Luz.
We prove the intermediate claim Lxvuz: SNo (x * v + u * z).
An exact proof term for the current goal is SNo_add_SNo (x * v) (u * z) Hxv Luz.
We prove the intermediate claim L1: u * y + x * z < x * y + u * z.
An exact proof term for the current goal is Hxy1 u Lux z Lzy.
We prove the intermediate claim L2: x * v + u * z < u * v + x * z.
An exact proof term for the current goal is Hxv3 u Lux z Lzv.
We will prove u * y + x * v < x * y + u * v.
Apply add_SNo_Lt2_cancel (x * z) (u * y + x * v) (x * y + u * v) Lxz Luyxv Lxyuv to the current goal.
We will prove x * z + u * y + x * v < x * z + x * y + u * v.
Apply SNoLt_tra (x * z + u * y + x * v) (x * y + u * z + x * v) (x * z + x * y + u * v) (SNo_add_SNo (x * z) (u * y + x * v) Lxz Luyxv) (SNo_add_SNo (x * y) (u * z + x * v) Hxy (SNo_add_SNo (u * z) (x * v) Luz Hxv)) (SNo_add_SNo (x * z) (x * y + u * v) Lxz Lxyuv) to the current goal.
We will prove x * z + u * y + x * v < x * y + u * z + x * v.
rewrite the current goal using add_SNo_assoc (x * z) (u * y) (x * v) Lxz Huy Hxv (from left to right).
rewrite the current goal using add_SNo_com (x * z) (u * y) Lxz Huy (from left to right).
We will prove (u * y + x * z) + x * v < x * y + u * z + x * v.
rewrite the current goal using add_SNo_assoc (x * y) (u * z) (x * v) Hxy Luz Hxv (from left to right).
An exact proof term for the current goal is add_SNo_Lt1 (u * y + x * z) (x * v) (x * y + u * z) Luyxz Hxv Lxyuz L1.
We will prove x * y + u * z + x * v < x * z + x * y + u * v.
rewrite the current goal using add_SNo_rotate_3_1 (x * y) (u * v) (x * z) Hxy Huv Lxz (from right to left).
We will prove x * y + u * z + x * v < x * y + u * v + x * z.
rewrite the current goal using add_SNo_com (u * z) (x * v) Luz Hxv (from left to right).
We will prove x * y + x * v + u * z < x * y + u * v + x * z.
An exact proof term for the current goal is add_SNo_Lt2 (x * y) (x * v + u * z) (u * v + x * z) Hxy Lxvuz Luvxz L2.
Assume H4: SNoLev v ∈ SNoLev y.
Assume H5: SNoEq_ (SNoLev v) v y.
Assume H6: SNoLev v ∈ y.
We prove the intermediate claim Lvy: v ∈ SNoL y.
An exact proof term for the current goal is SNoL_I y Hy v Hv H4 Hvy.
An exact proof term for the current goal is Hxy1 u Lux v Lvy.
Assume H4: SNoLev y ∈ SNoLev v.
Assume H5: SNoEq_ (SNoLev y) v y.
Assume H6: SNoLev y ∉ v.
We prove the intermediate claim Lyv: y ∈ SNoR v.
An exact proof term for the current goal is SNoR_I v Hv y Hy H4 Hvy.
We will prove u * y + x * v < x * y + u * v.
rewrite the current goal using add_SNo_com (u * y) (x * v) Huy Hxv (from left to right).
rewrite the current goal using add_SNo_com (x * y) (u * v) Hxy Huv (from left to right).
An exact proof term for the current goal is Hxv3 u Lux y Lyv.
Assume H1: SNoLev x ∈ SNoLev u.
Assume H2: SNoEq_ (SNoLev x) u x.
Assume H3: SNoLev x ∉ u.
We prove the intermediate claim Lxu: x ∈ SNoR u.
An exact proof term for the current goal is SNoR_I u Hu x Hx H1 Hux.
Apply SNoLtE v y Hv Hy Hvy to the current goal.
Let z be given.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev v ∩ SNoLev y.
Assume Hz3: SNoEq_ (SNoLev z) z v.
Assume Hz4: SNoEq_ (SNoLev z) z y.
Assume Hz5: v < z.
Assume Hz6: z < y.
Assume Hz7: SNoLev z ∉ v.
Assume Hz8: SNoLev z ∈ y.
Apply binintersectE (SNoLev v) (SNoLev y) (SNoLev z) Hz2 to the current goal.
Assume Hz2a Hz2b.
We prove the intermediate claim Lzy: z ∈ SNoL y.
An exact proof term for the current goal is SNoL_I y Hy z Hz1 Hz2b Hz6.
We prove the intermediate claim Lzv: z ∈ SNoR v.
An exact proof term for the current goal is SNoR_I v Hv z Hz1 Hz2a Hz5.
We prove the intermediate claim Lxz: SNo (x * z).
An exact proof term for the current goal is SNo_mul_SNo x z Hx Hz1.
We prove the intermediate claim Luz: SNo (u * z).
An exact proof term for the current goal is SNo_mul_SNo u z Hu Hz1.
We prove the intermediate claim L1: u * y + x * z < x * y + u * z.
An exact proof term for the current goal is Huy4 x Lxu z Lzy.
We prove the intermediate claim L2: x * v + u * z < u * v + x * z.
An exact proof term for the current goal is Huv2 x Lxu z Lzv.
We will prove u * y + x * v < x * y + u * v.
Apply add_SNo_Lt1_cancel (u * y + x * v) (x * z) (x * y + u * v) Luyxv Lxz Lxyuv to the current goal.
We will prove (u * y + x * v) + x * z < (x * y + u * v) + x * z.
rewrite the current goal using add_SNo_com (u * y) (x * v) Huy Hxv (from left to right).
We will prove (x * v + u * y) + x * z < (x * y + u * v) + x * z.
rewrite the current goal using add_SNo_assoc (x * v) (u * y) (x * z) Hxv Huy Lxz (from right to left).
rewrite the current goal using add_SNo_assoc (x * y) (u * v) (x * z) Hxy Huv Lxz (from right to left).
We will prove x * v + u * y + x * z < x * y + u * v + x * z.
We prove the intermediate claim Luyxz: SNo (u * y + x * z).
An exact proof term for the current goal is SNo_add_SNo (u * y) (x * z) Huy Lxz.
We prove the intermediate claim Luzxy: SNo (u * z + x * y).
An exact proof term for the current goal is SNo_add_SNo (u * z) (x * y) Luz Hxy.
We prove the intermediate claim Luvxz: SNo (u * v + x * z).
An exact proof term for the current goal is SNo_add_SNo (u * v) (x * z) Huv Lxz.
Apply SNoLt_tra (x * v + u * y + x * z) (x * v + u * z + x * y) (x * y + u * v + x * z) (SNo_add_SNo (x * v) (u * y + x * z) Hxv Luyxz) (SNo_add_SNo (x * v) (u * z + x * y) Hxv Luzxy) (SNo_add_SNo (x * y) (u * v + x * z) Hxy Luvxz) to the current goal.
We will prove x * v + u * y + x * z < x * v + u * z + x * y.
rewrite the current goal using add_SNo_com (u * z) (x * y) Luz Hxy (from left to right).
An exact proof term for the current goal is add_SNo_Lt2 (x * v) (u * y + x * z) (x * y + u * z) Hxv Luyxz (SNo_add_SNo (x * y) (u * z) Hxy Luz) L1.
We will prove x * v + u * z + x * y < x * y + u * v + x * z.
rewrite the current goal using add_SNo_rotate_3_1 (x * v) (u * z) (x * y) Hxv Luz Hxy (from left to right).
We will prove x * y + x * v + u * z < x * y + u * v + x * z.
An exact proof term for the current goal is add_SNo_Lt2 (x * y) (x * v + u * z) (u * v + x * z) Hxy (SNo_add_SNo (x * v) (u * z) Hxv Luz) Luvxz L2.
Assume H4: SNoLev v ∈ SNoLev y.
Assume H5: SNoEq_ (SNoLev v) v y.
Assume H6: SNoLev v ∈ y.
We prove the intermediate claim Lvy: v ∈ SNoL y.
An exact proof term for the current goal is SNoL_I y Hy v Hv H4 Hvy.
We will prove u * y + x * v < x * y + u * v.
An exact proof term for the current goal is Huy4 x Lxu v Lvy.
Assume H4: SNoLev y ∈ SNoLev v.
Assume H5: SNoEq_ (SNoLev y) v y.
Assume H6: SNoLev y ∉ v.
We prove the intermediate claim Lyv: y ∈ SNoR v.
An exact proof term for the current goal is SNoR_I v Hv y Hy H4 Hvy.
We will prove u * y + x * v < x * y + u * v.
rewrite the current goal using add_SNo_com (u * y) (x * v) Huy Hxv (from left to right).
rewrite the current goal using add_SNo_com (x * y) (u * v) Hxy Huv (from left to right).
An exact proof term for the current goal is Huv2 x Lxu y Lyv.
∎