Let x, y, z, w, u, a, b and c be given.
Assume Hx Hy Hz Hw Hu Ha Hb Hc H1 H2 H3.
We prove the intermediate claim L1: x + z < c + w.
Apply add_SNo_Lt_subprop2 x z c w a b Hx Hz Hc Hw Ha Hb to the current goal.
We will prove x + a < c + b.
rewrite the current goal using add_SNo_com c b Hc Hb (from left to right).
An exact proof term for the current goal is H1.
We will prove z + b < w + a.
rewrite the current goal using add_SNo_com z b Hz Hb (from left to right).
An exact proof term for the current goal is H3.
We prove the intermediate claim Lxz: SNo (x + z).
An exact proof term for the current goal is SNo_add_SNo x z Hx Hz.
We prove the intermediate claim Lcw: SNo (c + w).
An exact proof term for the current goal is SNo_add_SNo c w Hc Hw.
Apply SNoLt_tra (x + y + z) (c + w + y) (w + u) to the current goal.
An exact proof term for the current goal is SNo_add_SNo x (y + z) Hx (SNo_add_SNo y z Hy Hz).
An exact proof term for the current goal is SNo_add_SNo c (w + y) Hc (SNo_add_SNo w y Hw Hy).
An exact proof term for the current goal is SNo_add_SNo w u Hw Hu.
We will prove x + y + z < c + w + y.
rewrite the current goal using add_SNo_com y z Hy Hz (from left to right).
We will prove x + z + y < c + w + y.
rewrite the current goal using add_SNo_assoc x z y Hx Hz Hy (from left to right).
rewrite the current goal using add_SNo_assoc c w y Hc Hw Hy (from left to right).
An exact proof term for the current goal is add_SNo_Lt1 (x + z) y (c + w) Lxz Hy Lcw L1.
We will prove c + w + y < w + u.
rewrite the current goal using add_SNo_rotate_3_1 w y c Hw Hy Hc (from right to left).
We will prove w + y + c < w + u.
Apply add_SNo_Lt2 w (y + c) u Hw (SNo_add_SNo y c Hy Hc) Hu to the current goal.
We will prove y + c < u.
An exact proof term for the current goal is H2.
∎