Let x and y be given.
Assume Hx Hy.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Assume Hy1: y ∈ SNoR x.
Assume Hy2: SNo y.
Assume Hy3: ∀w ∈ SNoR x, SNo w → y ≤ w.
Apply SNoR_E x Hx y Hy1 to the current goal.
Assume Hy1a.
Assume Hy1b: SNoLev y ∈ SNoLev x.
Assume Hy1c: x < y.
Let z be given.
Assume Hz: SNo z.
Assume H1: z < x.
Assume H2: x + x < y + z.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate claim Lmy: SNo (- y).
An exact proof term for the current goal is SNo_minus_SNo y Hy2.
We prove the intermediate claim Lmz: SNo (- z).
An exact proof term for the current goal is SNo_minus_SNo z Hz.
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.
We prove the intermediate claim L1: SNo_max_of (SNoL (- x)) (- y).
rewrite the current goal using SNoL_minus_SNoR x Hx (from left to right).
We will prove SNo_max_of {- w|w ∈ SNoR x} (- y).
Apply minus_SNo_min_max to the current goal.
We will prove ∀w ∈ SNoR x, SNo w.
Let w be given.
Assume Hw.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 _ _.
An exact proof term for the current goal is Hw1.
We will prove SNo_min_of (SNoR x) y.
An exact proof term for the current goal is Hy.
We prove the intermediate claim L2: - x < - z.
An exact proof term for the current goal is minus_SNo_Lt_contra z x Hz Hx H1.
We prove the intermediate claim L3: - y + - z < - x + - x.
rewrite the current goal using minus_add_SNo_distr y z Hy2 Hz (from right to left).
rewrite the current goal using minus_add_SNo_distr x x Hx Hx (from right to left).
An exact proof term for the current goal is minus_SNo_Lt_contra (x + x) (y + z) Lxx Lyz H2.
Apply double_SNo_max_1 (- x) (- y) Lmx L1 (- z) Lmz L2 L3 to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR (- z).
rewrite the current goal using minus_add_SNo_distr x x Hx Hx (from right to left).
Assume H3: - y + w = - (x + x).
Apply SNoR_E (- z) Lmz w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev (- z).
Assume Hw3: - z < w.
We prove the intermediate claim Lmw: SNo (- w).
An exact proof term for the current goal is SNo_minus_SNo w Hw1.
We use (- w) to witness the existential quantifier.
Apply andI to the current goal.
We will prove - w ∈ SNoL z.
rewrite the current goal using minus_SNo_invol z Hz (from right to left).
We will prove - w ∈ SNoL (- - z).
rewrite the current goal using SNoL_minus_SNoR (- z) Lmz (from left to right).
We will prove - w ∈ {- w|w ∈ SNoR (- z)}.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hw.
We will prove y + - w = x + x.
rewrite the current goal using minus_SNo_invol (x + x) Lxx (from right to left).
We will prove y + - w = - - (x + x).
rewrite the current goal using H3 (from right to left).
We will prove y + - w = - (- y + w).
rewrite the current goal using minus_add_SNo_distr (- y) w Lmy Hw1 (from left to right).
We will prove y + - w = - - y + - w.
rewrite the current goal using minus_SNo_invol y Hy2 (from left to right).
Use reflexivity.
∎