Apply SNoLev_ind to the current goal.

Let u be given.

Assume Hu1: SNo u.

Assume IH: ∀z ∈ SNoS_ (SNoLev u), SNoLev z ∈ SNoLev (x * y) → z < x * y → P z.

Assume Hu2: SNoLev u ∈ SNoLev (x * y).

Assume Hu3: u < x * y.

Apply dneg to the current goal.

Assume HNC: ¬ P u.

We prove the intermediate claim L1: ∀v ∈ SNoL x, ∀w ∈ SNoL y, v * y + x * w < u + v * w.

Let v be given.

Assume Hv.

Let w be given.

Assume Hw.

Apply SNoL_E x Hx v Hv to the current goal.

Assume Hv1 Hv2 Hv3.

Apply SNoL_E y Hy w Hw to the current goal.

Assume Hw1 Hw2 Hw3.

Apply SNoLtLe_or (v * y + x * w) (u + v * w) (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Hv1 Hy) (SNo_mul_SNo x w Hx Hw1)) (SNo_add_SNo u (v * w) Hu1 (SNo_mul_SNo v w Hv1 Hw1)) to the current goal.

Assume H.

An exact proof term for the current goal is H.

Assume H.

Apply HNC to the current goal.

Apply orIL to the current goal.

We use v to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hv.

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 H.

We prove the intermediate claim L2: ∀v ∈ SNoR x, ∀w ∈ SNoR y, v * y + x * w < u + v * w.

Let v be given.

Assume Hv.

Let w be given.

Assume Hw.

Apply SNoR_E x Hx v Hv to the current goal.

Assume Hv1 Hv2 Hv3.

Apply SNoR_E y Hy w Hw to the current goal.

Assume Hw1 Hw2 Hw3.

Apply SNoLtLe_or (v * y + x * w) (u + v * w) (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Hv1 Hy) (SNo_mul_SNo x w Hx Hw1)) (SNo_add_SNo u (v * w) Hu1 (SNo_mul_SNo v w Hv1 Hw1)) to the current goal.

Assume H.

An exact proof term for the current goal is H.

Assume H.

Apply HNC to the current goal.

Apply orIR to the current goal.

We use v to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hv.

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 H.

Apply SNoLt_irref u to the current goal.

Apply SNoLtLe_tra u (x * y) u Hu1 Lxy Hu1 Hu3 to the current goal.

We will prove x * y ≤ u.

Apply mul_SNo_eq_3 x y Hx Hy to the current goal.

Let L and R be given.

Assume HLR HLE HLI1 HLI2 HRE HRI1 HRI2.

Assume HE: x * y = SNoCut L R.

rewrite the current goal using HE (from left to right).

We will prove SNoCut L R ≤ u.

rewrite the current goal using SNo_eta u Hu1 (from left to right).

We will prove SNoCut L R ≤ SNoCut (SNoL u) (SNoR u).

Apply SNoCut_Le L R (SNoL u) (SNoR u) HLR (SNoCutP_SNoL_SNoR u Hu1) to the current goal.

We will prove ∀z ∈ L, z < SNoCut (SNoL u) (SNoR u).

Let z be given.

Assume Hz.

rewrite the current goal using SNo_eta u Hu1 (from right to left).

We will prove z < u.

Apply HLE z Hz to the current goal.

Let v be given.

Assume Hv: v ∈ SNoL x.

Let w be given.

Assume Hw: w ∈ SNoL y.

Assume Hze: z = v * y + x * w + - v * w.

rewrite the current goal using Hze (from left to right).

We will prove v * y + x * w + - v * w < u.

Apply SNoL_E x Hx v Hv to the current goal.

Assume Hv1 Hv2 Hv3.

Apply SNoL_E y Hy w Hw to the current goal.

Assume Hw1 Hw2 Hw3.

Apply add_SNo_minus_Lt1b3 (v * y) (x * w) (v * w) u (SNo_mul_SNo v y Hv1 Hy) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v w Hv1 Hw1) Hu1 to the current goal.

We will prove v * y + x * w < u + v * w.

An exact proof term for the current goal is L1 v Hv w Hw.

Let v be given.

Assume Hv: v ∈ SNoR x.

Let w be given.

Assume Hw: w ∈ SNoR y.

Assume Hze: z = v * y + x * w + - v * w.

rewrite the current goal using Hze (from left to right).

We will prove v * y + x * w + - v * w < u.

Apply SNoR_E x Hx v Hv to the current goal.

Assume Hv1 Hv2 Hv3.

Apply SNoR_E y Hy w Hw to the current goal.

Assume Hw1 Hw2 Hw3.

Apply add_SNo_minus_Lt1b3 (v * y) (x * w) (v * w) u (SNo_mul_SNo v y Hv1 Hy) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v w Hv1 Hw1) Hu1 to the current goal.

We will prove v * y + x * w < u + v * w.

An exact proof term for the current goal is L2 v Hv w Hw.

We will prove ∀z ∈ SNoR u, SNoCut L R < z.

Let z be given.

Assume Hz: z ∈ SNoR u.

rewrite the current goal using HE (from right to left).

We will prove x * y < z.

Apply SNoR_E u Hu1 z Hz to the current goal.

Assume Hz1: SNo z.

Assume Hz2: SNoLev z ∈ SNoLev u.

Assume Hz3: u < z.

Apply SNoLt_trichotomy_or_impred z (x * y) Hz1 Lxy to the current goal.

Assume H1: z < x * y.

We prove the intermediate claim LPz: P z.

Apply IH z to the current goal.

We will prove z ∈ SNoS_ (SNoLev u).

Apply SNoS_I2 to the current goal.

An exact proof term for the current goal is Hz1.

An exact proof term for the current goal is Hu1.

An exact proof term for the current goal is Hz2.

We will prove SNoLev z ∈ SNoLev (x * y).

An exact proof term for the current goal is ordinal_TransSet (SNoLev (x * y)) (SNoLev_ordinal (x * y) Lxy) (SNoLev u) Hu2 (SNoLev z) Hz2.

We will prove z < x * y.

An exact proof term for the current goal is H1.

Apply LPz to the current goal.

Assume H2: P1 z.

Apply H2 to the current goal.

Let v be given.

Assume H2.

Apply H2 to the current goal.

Assume Hv: v ∈ SNoL x.

Assume H2.

Apply H2 to the current goal.

Let w be given.

Assume H2.

Apply H2 to the current goal.

Assume Hw: w ∈ SNoL y.

Assume Hvw: z + v * w ≤ v * y + x * w.

Apply SNoL_E x Hx v Hv to the current goal.

Assume Hv1 Hv2 Hv3.

Apply SNoL_E y Hy w Hw to the current goal.

Assume Hw1 Hw2 Hw3.

We prove the intermediate claim Lvw: SNo (v * w).

An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.

We prove the intermediate claim L3: z + v * w < u + v * w.

Apply SNoLeLt_tra (z + v * w) (v * y + x * w) (u + v * w) (SNo_add_SNo z (v * w) Hz1 Lvw) (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Hv1 Hy) (SNo_mul_SNo x w Hx Hw1)) (SNo_add_SNo u (v * w) Hu1 Lvw) Hvw to the current goal.

We will prove v * y + x * w < u + v * w.

An exact proof term for the current goal is L1 v Hv w Hw.

We prove the intermediate claim L4: z < u.

An exact proof term for the current goal is add_SNo_Lt1_cancel z (v * w) u Hz1 Lvw Hu1 L3.

Apply SNoLt_irref u to the current goal.

An exact proof term for the current goal is SNoLt_tra u z u Hu1 Hz1 Hu1 Hz3 L4.

Assume H2: P2 z.

Apply H2 to the current goal.

Let v be given.

Assume H2.

Apply H2 to the current goal.

Assume Hv: v ∈ SNoR x.

Assume H2.

Apply H2 to the current goal.

Let w be given.

Assume H2.

Apply H2 to the current goal.

Assume Hw: w ∈ SNoR y.

Assume Hvw: z + v * w ≤ v * y + x * w.

Apply SNoR_E x Hx v Hv to the current goal.

Assume Hv1 Hv2 Hv3.

Apply SNoR_E y Hy w Hw to the current goal.

Assume Hw1 Hw2 Hw3.

We prove the intermediate claim Lvw: SNo (v * w).

An exact proof term for the current goal is SNo_mul_SNo v w Hv1 Hw1.

We prove the intermediate claim L5: z + v * w < u + v * w.

We will prove v * y + x * w < u + v * w.

An exact proof term for the current goal is L2 v Hv w Hw.

We prove the intermediate claim L6: z < u.

An exact proof term for the current goal is add_SNo_Lt1_cancel z (v * w) u Hz1 Lvw Hu1 L5.

Apply SNoLt_irref u to the current goal.

An exact proof term for the current goal is SNoLt_tra u z u Hu1 Hz1 Hu1 Hz3 L6.

Assume H1: z = x * y.

Apply In_no2cycle (SNoLev u) (SNoLev (x * y)) Hu2 to the current goal.

We will prove SNoLev (x * y) ∈ SNoLev u.

rewrite the current goal using H1 (from right to left).

An exact proof term for the current goal is Hz2.

Assume H1: x * y < z.

An exact proof term for the current goal is H1.