Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx.
Assume IHx: ∀w ∈ SNoS_ (SNoLev x), w * 1 = w.
Apply mul_SNo_eq_3 x 1 Hx SNo_1 to the current goal.
Let L and R be given.
Assume HLR HLE HLI1 HLI2 HRE HRI1 HRI2 Hx1e.
We will prove x * 1 = x.
Apply mul_SNo_prop_1 x Hx 1 SNo_1 to the current goal.
Assume Hx1: SNo (x * 1).
Assume Hx11: ∀u ∈ SNoL x, ∀v ∈ SNoL 1, u * 1 + x * v < x * 1 + u * v.
Assume Hx12: ∀u ∈ SNoR x, ∀v ∈ SNoR 1, u * 1 + x * v < x * 1 + u * v.
Assume Hx13: ∀u ∈ SNoL x, ∀v ∈ SNoR 1, x * 1 + u * v < u * 1 + x * v.
Assume Hx14: ∀u ∈ SNoR x, ∀v ∈ SNoL 1, x * 1 + u * v < u * 1 + x * v.
We prove the intermediate claim L0L1: 0 ∈ SNoL 1.
rewrite the current goal using SNoL_1 (from left to right).
An exact proof term for the current goal is In_0_1.
rewrite the current goal using Hx1e (from left to right).
We will prove SNoCut L R = x.
rewrite the current goal using SNo_eta x Hx (from left to right).
We will prove SNoCut L R = SNoCut (SNoL x) (SNoR x).
Apply SNoCut_ext L R (SNoL x) (SNoR x) HLR (SNoCutP_SNoL_SNoR x Hx) to the current goal.
We will prove ∀w ∈ L, w < SNoCut (SNoL x) (SNoR x).
Let w be given.
Assume Hw.
Apply SNoCutP_SNoCut_L (SNoL x) (SNoR x) (SNoCutP_SNoL_SNoR x Hx) to the current goal.
We will prove w ∈ SNoL x.
Apply HLE w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Let v be given.
rewrite the current goal using SNoL_1 (from left to right).
Assume Hv: v ∈ 1.
Apply cases_1 v Hv to the current goal.
Assume Hwuv: w = u * 1 + x * 0 + - u * 0.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hua _ _.
We prove the intermediate claim L1: w = u.
rewrite the current goal using Hwuv (from left to right).
Use transitivity with u * 1 + 0, and u * 1.
We will prove u * 1 + x * 0 + - u * 0 = u * 1 + 0.
Use f_equal.
We will prove x * 0 + - u * 0 = 0.
Use transitivity with x * 0 + 0, and x * 0.
We will prove x * 0 + - u * 0 = x * 0 + 0.
Use f_equal.
We will prove - u * 0 = 0.
Use transitivity with and - 0.
We will prove - u * 0 = - 0.
Use f_equal.
An exact proof term for the current goal is mul_SNo_zeroR u Hua.
An exact proof term for the current goal is minus_SNo_0.
We will prove x * 0 + 0 = x * 0.
An exact proof term for the current goal is add_SNo_0R (x * 0) (SNo_mul_SNo x 0 Hx SNo_0).
We will prove x * 0 = 0.
An exact proof term for the current goal is mul_SNo_zeroR x Hx.
We will prove u * 1 + 0 = u * 1.
An exact proof term for the current goal is add_SNo_0R (u * 1) (SNo_mul_SNo u 1 Hua SNo_1).
We will prove u * 1 = u.
An exact proof term for the current goal is IHx u (SNoL_SNoS x Hx u Hu).
rewrite the current goal using L1 (from left to right).
An exact proof term for the current goal is Hu.
Let u be given.
Assume Hu: u ∈ SNoR x.
Let v be given.
rewrite the current goal using SNoR_1 (from left to right).
Assume Hv: v ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE v Hv.
We will prove ∀z ∈ R, SNoCut (SNoL x) (SNoR x) < z.
Let z be given.
Assume Hz.
Apply SNoCutP_SNoCut_R (SNoL x) (SNoR x) (SNoCutP_SNoL_SNoR x Hx) to the current goal.
We will prove z ∈ SNoR x.
Apply HRE z Hz to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Let v be given.
rewrite the current goal using SNoR_1 (from left to right).
Assume Hv: v ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE v Hv.
Let u be given.
Assume Hu: u ∈ SNoR x.
Let v be given.
rewrite the current goal using SNoL_1 (from left to right).
Assume Hv: v ∈ 1.
Apply cases_1 v Hv to the current goal.
Assume Hzuv: z = u * 1 + x * 0 + - u * 0.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hua _ _.
We prove the intermediate claim L1: z = u.
rewrite the current goal using Hzuv (from left to right).
Use transitivity with u * 1 + 0, and u * 1.
We will prove u * 1 + x * 0 + - u * 0 = u * 1 + 0.
Use f_equal.
We will prove x * 0 + - u * 0 = 0.
Use transitivity with x * 0 + 0, and x * 0.
We will prove x * 0 + - u * 0 = x * 0 + 0.
Use f_equal.
We will prove - u * 0 = 0.
Use transitivity with and - 0.
We will prove - u * 0 = - 0.
Use f_equal.
An exact proof term for the current goal is mul_SNo_zeroR u Hua.
An exact proof term for the current goal is minus_SNo_0.
We will prove x * 0 + 0 = x * 0.
An exact proof term for the current goal is add_SNo_0R (x * 0) (SNo_mul_SNo x 0 Hx SNo_0).
We will prove x * 0 = 0.
An exact proof term for the current goal is mul_SNo_zeroR x Hx.
We will prove u * 1 + 0 = u * 1.
An exact proof term for the current goal is add_SNo_0R (u * 1) (SNo_mul_SNo u 1 Hua SNo_1).
We will prove u * 1 = u.
An exact proof term for the current goal is IHx u (SNoR_SNoS x Hx u Hu).
rewrite the current goal using L1 (from left to right).
An exact proof term for the current goal is Hu.
We will prove ∀w ∈ SNoL x, w < SNoCut L R.
Let w be given.
Assume Hw.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hwa _ _.
rewrite the current goal using Hx1e (from right to left).
We will prove w < x * 1.
We prove the intermediate claim L1: w * 1 + x * 0 = w.
Use transitivity with w * 1 + 0, and w * 1.
Use f_equal.
We will prove x * 0 = 0.
An exact proof term for the current goal is mul_SNo_zeroR x Hx.
An exact proof term for the current goal is add_SNo_0R (w * 1) (SNo_mul_SNo w 1 Hwa SNo_1).
An exact proof term for the current goal is IHx w (SNoL_SNoS x Hx w Hw).
We prove the intermediate claim L2: x * 1 + w * 0 = x * 1.
Use transitivity with and x * 1 + 0.
Use f_equal.
An exact proof term for the current goal is mul_SNo_zeroR w Hwa.
An exact proof term for the current goal is add_SNo_0R (x * 1) (SNo_mul_SNo x 1 Hx SNo_1).
rewrite the current goal using L1 (from right to left).
rewrite the current goal using L2 (from right to left).
We will prove w * 1 + x * 0 < x * 1 + w * 0.
An exact proof term for the current goal is Hx11 w Hw 0 L0L1.
We will prove ∀z ∈ SNoR x, SNoCut L R < z.
Let z be given.
Assume Hz.
Apply SNoR_E x Hx z Hz to the current goal.
Assume Hza _ _.
rewrite the current goal using Hx1e (from right to left).
We will prove x * 1 < z.
We prove the intermediate claim L1: x * 1 + z * 0 = x * 1.
Use transitivity with and x * 1 + 0.
Use f_equal.
An exact proof term for the current goal is mul_SNo_zeroR z Hza.
An exact proof term for the current goal is add_SNo_0R (x * 1) (SNo_mul_SNo x 1 Hx SNo_1).
We prove the intermediate claim L2: z * 1 + x * 0 = z.
Use transitivity with z * 1 + 0, and z * 1.
Use f_equal.
We will prove x * 0 = 0.
An exact proof term for the current goal is mul_SNo_zeroR x Hx.
An exact proof term for the current goal is add_SNo_0R (z * 1) (SNo_mul_SNo z 1 Hza SNo_1).
An exact proof term for the current goal is IHx z (SNoR_SNoS x Hx z Hz).
rewrite the current goal using L2 (from right to left).
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is Hx14 z Hz 0 L0L1.
∎