Let x and y be given.
Assume Hx Hy.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Apply SNoL_E x Hx y Hy1 to the current goal.
Assume Hy1a.
Let z be given.
We prove the intermediate
claim Lxx:
SNo (x + x).
An
exact proof term for the current goal is
SNo_add_SNo x x Hx Hx.
We prove the intermediate
claim Lyz:
SNo (y + z).
An
exact proof term for the current goal is
SNo_add_SNo y z Hy2 Hz.
Let w be given.
Assume Hw.
Apply SNoR_E y Hy2 w Hw to the current goal.
We will
prove x + x < x + x.
We will
prove x + x < w + z.
Apply add_SNo_Lt3b x x w z Hx Hx Hw1 Hz to the current goal.
We prove the intermediate
claim L1a:
w ∈ SNoL x.
Apply SNoL_I x Hx w Hw1 to the current goal.
An exact proof term for the current goal is H4.
Apply SNoLtLe_tra y w y Hy2 Hw1 Hy2 Hw3 to the current goal.
An exact proof term for the current goal is Hy3 w L1a Hw1.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H1.
We will
prove w + z ≤ x + x.
An exact proof term for the current goal is H3.
Let w be given.
Assume Hw.
Apply SNoL_E x Hx w Hw to the current goal.
We will
prove w + x < w + x.
We will
prove w + x < w + z.
An exact proof term for the current goal is H1.
We will
prove w + z ≤ w + x.
We will
prove w + z ≤ y + z.
Apply add_SNo_Le1 w z y Hw1 Hz Hy2 to the current goal.
An exact proof term for the current goal is Hy3 w Hw Hw1.
We will
prove y + z ≤ w + x.
An exact proof term for the current goal is H3.
Let w be given.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw2.
We prove the intermediate
claim LIH:
∃u ∈ SNoR w, y + u = x + x.
Apply IH w (SNoR_SNoS_ z w Hw) to the current goal.
An
exact proof term for the current goal is
SNoLt_tra x z w Hx Hz Hw1 H1 Hw3.
We will
prove y + w < x + x.
An exact proof term for the current goal is H4.
Apply LIH to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Apply SNoR_E w Hw1 u Hu1 to the current goal.
Assume Hu1a Hu1b Hu1c.
We use u to witness the existential quantifier.
Apply andI to the current goal.
We will
prove u ∈ SNoR z.
Apply SNoR_I z Hz u Hu1a to the current goal.
An
exact proof term for the current goal is
SNoLt_tra z w u Hz Hw1 Hu1a Hw3 Hu1c.
An exact proof term for the current goal is Hu2.
Let u be given.
Apply SNoL_E (x + x) Lxx u Hu1 to the current goal.
Assume Hu1b.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Apply SNoR_E y Hy2 w Hw to the current goal.
Assume Hw2.
Apply L1 w Hw to the current goal.
We will
prove w + z ≤ x + x.
We will
prove w + z < x + x.
An exact proof term for the current goal is Hu1c.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Apply SNoR_E z Hz w Hw to the current goal.
Assume Hw2.
Apply L3 w Hw to the current goal.
We will
prove y + w < x + x.
An exact proof term for the current goal is Hu1c.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
An exact proof term for the current goal is L2 w Hw H4.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply L2 w Hw to the current goal.
We will
prove y + z ≤ w + x.
rewrite the current goal using
add_SNo_com w x Hw1 Hx (from left to right).
We will
prove y + z ≤ x + w.
An exact proof term for the current goal is H4.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
An exact proof term for the current goal is L1 w Hw H4.
Assume H.
Apply H to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Apply SNoR_E z Hz w Hw to the current goal.
Apply L3 w Hw to the current goal.
We will
prove y + w < x + x.
An exact proof term for the current goal is H5.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
∎