Let x, y, w, u, v, a, b and c be given.
Assume Hx Hy Hw Hu Hv Ha Hb Hc H1 H2 H3.
We prove the intermediate claim L1: b + y < w + u + a.
An exact proof term for the current goal is add_SNo_Lt_subprop3b b y w u a c Hb Hy Hw Hu Ha Hc H3 H2.
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 Lwuv: SNo (w + u + v).
An exact proof term for the current goal is SNo_add_SNo w (u + v) Hw (SNo_add_SNo u v Hu Hv).
We prove the intermediate claim Lwua: SNo (w + u + a).
An exact proof term for the current goal is SNo_add_SNo w (u + a) Hw (SNo_add_SNo u a Hu Ha).
We prove the intermediate claim Lby: SNo (b + y).
An exact proof term for the current goal is SNo_add_SNo b y Hb Hy.
Apply add_SNo_Lt1_cancel (x + y) b (w + u + v) Lxy Hb Lwuv to the current goal.
We will prove (x + y) + b < (w + u + v) + b.
Apply SNoLt_tra ((x + y) + b) (x + w + u + a) ((w + u + v) + b) (SNo_add_SNo (x + y) b Lxy Hb) (SNo_add_SNo x (w + u + a) Hx Lwua) (SNo_add_SNo (w + u + v) b Lwuv Hb) to the current goal.
We will prove (x + y) + b < x + w + u + a.
rewrite the current goal using add_SNo_assoc x y b Hx Hy Hb (from right to left).
We will prove x + y + b < x + w + u + a.
rewrite the current goal using add_SNo_com y b Hy Hb (from left to right).
We will prove x + b + y < x + w + u + a.
Apply add_SNo_Lt2 x (b + y) (w + u + a) Hx Lby Lwua to the current goal.
We will prove b + y < w + u + a.
An exact proof term for the current goal is L1.
We will prove x + w + u + a < (w + u + v) + b.
We prove the intermediate claim L2: x + w + u + a = (w + u) + (x + a).
Use transitivity with (x + w + u) + a, (w + u + x) + a, and w + u + x + a.
An exact proof term for the current goal is add_SNo_assoc_4 x w u a Hx Hw Hu Ha.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is add_SNo_rotate_3_1 w u x Hw Hu Hx.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc_4 w u x a Hw Hu Hx Ha.
We will prove w + u + x + a = (w + u) + (x + a).
An exact proof term for the current goal is add_SNo_assoc w u (x + a) Hw Hu (SNo_add_SNo x a Hx Ha).
We prove the intermediate claim L3: (w + u + v) + b = (w + u) + b + v.
Use transitivity with ((w + u) + v) + b, and (w + u) + (v + b).
Use f_equal.
An exact proof term for the current goal is add_SNo_assoc w u v Hw Hu Hv.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc (w + u) v b (SNo_add_SNo w u Hw Hu) Hv Hb.
Use f_equal.
An exact proof term for the current goal is add_SNo_com v b Hv Hb.
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 (from left to right).
We will prove (w + u) + (x + a) < (w + u) + (b + v).
Apply add_SNo_Lt2 (w + u) (x + a) (b + v) (SNo_add_SNo w u Hw Hu) (SNo_add_SNo x a Hx Ha) (SNo_add_SNo b v Hb Hv) to the current goal.
An exact proof term for the current goal is H1.
∎