Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), - w + w = 0.
We will prove - x + x = 0.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
Set L1 to be the term {w + x|w ∈ SNoL (- x)}.
Set L2 to be the term {- x + w|w ∈ SNoL x}.
Set R1 to be the term {z + x|z ∈ SNoR (- x)}.
Set R2 to be the term {- x + z|z ∈ SNoR x}.
Set L to be the term L1 ∪ L2.
Set R to be the term R1 ∪ R2.
rewrite the current goal using add_SNo_eq (- x) Lmx x Hx (from left to right).
We will prove SNoCut L R = 0.
We prove the intermediate claim LLR: SNoCutP L R.
An exact proof term for the current goal is add_SNo_SNoCutP (- x) x Lmx Hx.
We prove the intermediate claim LNLR: SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R LLR.
We prove the intermediate claim Lfst: SNoLev (SNoCut L R) ⊆ SNoLev 0 ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) 0.
Apply SNoCutP_SNoCut_fst L R LLR 0 SNo_0 to the current goal.
We will prove ∀w ∈ L, w < 0.
Let w be given.
Assume Hw: w ∈ L.
Apply binunionE L1 L2 w Hw to the current goal.
Assume Hw: w ∈ {w + x|w ∈ SNoL (- x)}.
Apply ReplE_impred (SNoL (- x)) (λz ⇒ z + x) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL (- x).
Assume Hwu: w = u + x.
Apply SNoL_E (- x) Lmx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (- x).
Assume Hu3: u < - x.
We prove the intermediate claim Lmu: SNo (- u).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hu1.
We prove the intermediate claim Lmuu: - u + u = 0.
Apply IH to the current goal.
We will prove u ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 u x Hu1 Hx to the current goal.
We will prove SNoLev u ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev x Hx (from right to left).
We will prove SNoLev u ∈ SNoLev (- x).
An exact proof term for the current goal is Hu2.
We prove the intermediate claim Lxmu: x < - u.
rewrite the current goal using minus_SNo_invol x Hx (from right to left).
We will prove - - x < - u.
Apply minus_SNo_Lt_contra u (- x) Hu1 Lmx to the current goal.
We will prove u < - x.
An exact proof term for the current goal is Hu3.
We will prove w < 0.
rewrite the current goal using Hwu (from left to right).
We will prove u + x < 0.
rewrite the current goal using add_SNo_com u x Hu1 Hx (from left to right).
We will prove x + u < 0.
rewrite the current goal using Lmuu (from right to left).
We will prove x + u < - u + u.
Apply add_SNo_Lt1 x u (- u) Hx Hu1 Lmu to the current goal.
We will prove x < - u.
An exact proof term for the current goal is Lxmu.
Assume Hw: w ∈ {- x + w|w ∈ SNoL x}.
Apply ReplE_impred (SNoL x) (λz ⇒ - x + z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = - x + u.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: u < x.
We prove the intermediate claim Lmu: SNo (- u).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hu1.
We prove the intermediate claim Lmuu: - u + u = 0.
Apply IH to the current goal.
We will prove u ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 u x Hu1 Hx to the current goal.
We will prove SNoLev u ∈ SNoLev x.
An exact proof term for the current goal is Hu2.
We prove the intermediate claim Lmxmu: - x < - u.
Apply minus_SNo_Lt_contra u x Hu1 Hx to the current goal.
We will prove u < x.
An exact proof term for the current goal is Hu3.
We will prove w < 0.
rewrite the current goal using Hwu (from left to right).
We will prove - x + u < 0.
rewrite the current goal using Lmuu (from right to left).
We will prove - x + u < - u + u.
Apply add_SNo_Lt1 (- x) u (- u) Lmx Hu1 Lmu to the current goal.
We will prove - x < - u.
An exact proof term for the current goal is Lmxmu.
We will prove ∀z ∈ R, 0 < z.
Let z be given.
Assume Hz: z ∈ R.
Apply binunionE R1 R2 z Hz to the current goal.
Assume Hz: z ∈ {z + x|z ∈ SNoR (- x)}.
Apply ReplE_impred (SNoR (- x)) (λz ⇒ z + x) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoR (- x).
Assume Hzv: z = v + x.
Apply SNoR_E (- x) Lmx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev (- x).
Assume Hv3: - x < v.
We prove the intermediate claim Lmv: SNo (- v).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hv1.
We prove the intermediate claim Lmvv: - v + v = 0.
Apply IH to the current goal.
We will prove v ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 v x Hv1 Hx to the current goal.
We will prove SNoLev v ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev x Hx (from right to left).
We will prove SNoLev v ∈ SNoLev (- x).
An exact proof term for the current goal is Hv2.
We prove the intermediate claim Lmvx: - v < x.
rewrite the current goal using minus_SNo_invol x Hx (from right to left).
We will prove - v < - - x.
Apply minus_SNo_Lt_contra (- x) v Lmx Hv1 to the current goal.
We will prove - x < v.
An exact proof term for the current goal is Hv3.
We will prove 0 < z.
rewrite the current goal using Hzv (from left to right).
We will prove 0 < v + x.
rewrite the current goal using add_SNo_com v x Hv1 Hx (from left to right).
We will prove 0 < x + v.
rewrite the current goal using Lmvv (from right to left).
We will prove - v + v < x + v.
Apply add_SNo_Lt1 (- v) v x Lmv Hv1 Hx to the current goal.
We will prove - v < x.
An exact proof term for the current goal is Lmvx.
Assume Hz: z ∈ {- x + z|z ∈ SNoR x}.
Apply ReplE_impred (SNoR x) (λz ⇒ - x + z) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoR x.
Assume Hzv: z = - x + v.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: x < v.
We prove the intermediate claim Lmv: SNo (- v).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hv1.
We prove the intermediate claim Lmvv: - v + v = 0.
Apply IH to the current goal.
We will prove v ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 v x Hv1 Hx to the current goal.
We will prove SNoLev v ∈ SNoLev x.
An exact proof term for the current goal is Hv2.
We prove the intermediate claim Lmvmx: - v < - x.
Apply minus_SNo_Lt_contra x v Hx Hv1 to the current goal.
We will prove x < v.
An exact proof term for the current goal is Hv3.
We will prove 0 < z.
rewrite the current goal using Hzv (from left to right).
We will prove 0 < - x + v.
rewrite the current goal using Lmvv (from right to left).
We will prove - v + v < - x + v.
Apply add_SNo_Lt1 (- v) v (- x) Lmv Hv1 Lmx to the current goal.
We will prove - v < - x.
An exact proof term for the current goal is Lmvmx.
Apply Lfst to the current goal.
Assume H1: SNoLev (SNoCut L R) ⊆ SNoLev 0.
Assume H2: SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) 0.
Apply SNo_eq (SNoCut L R) 0 LNLR SNo_0 to the current goal.
We will prove SNoLev (SNoCut L R) = SNoLev 0.
Apply set_ext to the current goal.
An exact proof term for the current goal is H1.
rewrite the current goal using ordinal_SNoLev 0 ordinal_Empty (from left to right).
We will prove 0 ⊆ SNoLev (SNoCut L R).
Apply Subq_Empty to the current goal.
We will prove SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) 0.
An exact proof term for the current goal is H2.
∎