Apply SNoLev_ind2 to the current goal.
Let x and y be given.
Assume Hx Hy.
Assume IHx: ∀w ∈ SNoS_ (SNoLev x), w * y = y * w.
Assume IHy: ∀z ∈ SNoS_ (SNoLev y), x * z = z * x.
Assume IHxy: ∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), w * z = z * w.
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 Hxye.
Apply mul_SNo_eq_3 y x Hy Hx to the current goal.
Let L' and R' be given.
Assume HL'R' HL'E HL'I1 HL'I2 HR'E HR'I1 HR'I2 Hyxe.
rewrite the current goal using Hxye (from left to right).
rewrite the current goal using Hyxe (from left to right).
We will prove SNoCut L R = SNoCut L' R'.
We prove the intermediate claim LLL': L = L'.
Apply set_ext to the current goal.
We will prove L ⊆ L'.
Apply mul_SNo_Subq_lem x y (SNoL x) (SNoL y) (SNoR x) (SNoR y) L L' HLE to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Let v be given.
Assume Hv: v ∈ SNoL y.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using IHx u (SNoL_SNoS x Hx u Hu) (from left to right).
rewrite the current goal using IHy v (SNoL_SNoS y Hy v Hv) (from left to right).
rewrite the current goal using IHxy u (SNoL_SNoS x Hx u Hu) v (SNoL_SNoS y Hy v Hv) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (y * u) (v * x) (- v * u) (SNo_mul_SNo y u Hy Hua) (SNo_mul_SNo v x Hva Hx) (SNo_minus_SNo (v * u) (SNo_mul_SNo v u Hva Hua)) (from left to right).
Apply HL'I1 to the current goal.
An exact proof term for the current goal is Hv.
An exact proof term for the current goal is Hu.
Let u be given.
Assume Hu: u ∈ SNoR x.
Let v be given.
Assume Hv: v ∈ SNoR y.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using IHx u (SNoR_SNoS x Hx u Hu) (from left to right).
rewrite the current goal using IHy v (SNoR_SNoS y Hy v Hv) (from left to right).
rewrite the current goal using IHxy u (SNoR_SNoS x Hx u Hu) v (SNoR_SNoS y Hy v Hv) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (y * u) (v * x) (- v * u) (SNo_mul_SNo y u Hy Hua) (SNo_mul_SNo v x Hva Hx) (SNo_minus_SNo (v * u) (SNo_mul_SNo v u Hva Hua)) (from left to right).
Apply HL'I2 to the current goal.
An exact proof term for the current goal is Hv.
An exact proof term for the current goal is Hu.
We will prove L' ⊆ L.
Apply mul_SNo_Subq_lem y x (SNoL y) (SNoL x) (SNoR y) (SNoR x) L' L HL'E to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL y.
Let u be given.
Assume Hu: u ∈ SNoL x.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using IHx u (SNoL_SNoS x Hx u Hu) (from right to left).
rewrite the current goal using IHy v (SNoL_SNoS y Hy v Hv) (from right to left).
rewrite the current goal using IHxy u (SNoL_SNoS x Hx u Hu) v (SNoL_SNoS y Hy v Hv) (from right to left).
rewrite the current goal using add_SNo_com_3_0_1 (x * v) (u * y) (- u * v) (SNo_mul_SNo x v Hx Hva) (SNo_mul_SNo u y Hua Hy) (SNo_minus_SNo (u * v) (SNo_mul_SNo u v Hua Hva)) (from left to right).
Apply HLI1 to the current goal.
An exact proof term for the current goal is Hu.
An exact proof term for the current goal is Hv.
Let v be given.
Assume Hv: v ∈ SNoR y.
Let u be given.
Assume Hu: u ∈ SNoR x.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using IHx u (SNoR_SNoS x Hx u Hu) (from right to left).
rewrite the current goal using IHy v (SNoR_SNoS y Hy v Hv) (from right to left).
rewrite the current goal using IHxy u (SNoR_SNoS x Hx u Hu) v (SNoR_SNoS y Hy v Hv) (from right to left).
rewrite the current goal using add_SNo_com_3_0_1 (x * v) (u * y) (- u * v) (SNo_mul_SNo x v Hx Hva) (SNo_mul_SNo u y Hua Hy) (SNo_minus_SNo (u * v) (SNo_mul_SNo u v Hua Hva)) (from left to right).
Apply HLI2 to the current goal.
An exact proof term for the current goal is Hu.
An exact proof term for the current goal is Hv.
We prove the intermediate claim LRR': R = R'.
Apply set_ext to the current goal.
Apply mul_SNo_Subq_lem x y (SNoL x) (SNoR y) (SNoR x) (SNoL y) R R' HRE to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Let v be given.
Assume Hv: v ∈ SNoR y.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using IHx u (SNoL_SNoS x Hx u Hu) (from left to right).
rewrite the current goal using IHy v (SNoR_SNoS y Hy v Hv) (from left to right).
rewrite the current goal using IHxy u (SNoL_SNoS x Hx u Hu) v (SNoR_SNoS y Hy v Hv) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (y * u) (v * x) (- v * u) (SNo_mul_SNo y u Hy Hua) (SNo_mul_SNo v x Hva Hx) (SNo_minus_SNo (v * u) (SNo_mul_SNo v u Hva Hua)) (from left to right).
Apply HR'I2 to the current goal.
An exact proof term for the current goal is Hv.
An exact proof term for the current goal is Hu.
Let u be given.
Assume Hu: u ∈ SNoR x.
Let v be given.
Assume Hv: v ∈ SNoL y.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using IHx u (SNoR_SNoS x Hx u Hu) (from left to right).
rewrite the current goal using IHy v (SNoL_SNoS y Hy v Hv) (from left to right).
rewrite the current goal using IHxy u (SNoR_SNoS x Hx u Hu) v (SNoL_SNoS y Hy v Hv) (from left to right).
rewrite the current goal using add_SNo_com_3_0_1 (y * u) (v * x) (- v * u) (SNo_mul_SNo y u Hy Hua) (SNo_mul_SNo v x Hva Hx) (SNo_minus_SNo (v * u) (SNo_mul_SNo v u Hva Hua)) (from left to right).
Apply HR'I1 to the current goal.
An exact proof term for the current goal is Hv.
An exact proof term for the current goal is Hu.
Apply mul_SNo_Subq_lem y x (SNoL y) (SNoR x) (SNoR y) (SNoL x) R' R HR'E to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL y.
Let u be given.
Assume Hu: u ∈ SNoR x.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using IHx u (SNoR_SNoS x Hx u Hu) (from right to left).
rewrite the current goal using IHy v (SNoL_SNoS y Hy v Hv) (from right to left).
rewrite the current goal using IHxy u (SNoR_SNoS x Hx u Hu) v (SNoL_SNoS y Hy v Hv) (from right to left).
rewrite the current goal using add_SNo_com_3_0_1 (x * v) (u * y) (- u * v) (SNo_mul_SNo x v Hx Hva) (SNo_mul_SNo u y Hua Hy) (SNo_minus_SNo (u * v) (SNo_mul_SNo u v Hua Hva)) (from left to right).
Apply HRI2 to the current goal.
An exact proof term for the current goal is Hu.
An exact proof term for the current goal is Hv.
Let v be given.
Assume Hv: v ∈ SNoR y.
Let u be given.
Assume Hu: u ∈ SNoL x.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hua _ _.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
rewrite the current goal using IHx u (SNoL_SNoS x Hx u Hu) (from right to left).
rewrite the current goal using IHy v (SNoR_SNoS y Hy v Hv) (from right to left).
rewrite the current goal using IHxy u (SNoL_SNoS x Hx u Hu) v (SNoR_SNoS y Hy v Hv) (from right to left).
rewrite the current goal using add_SNo_com_3_0_1 (x * v) (u * y) (- u * v) (SNo_mul_SNo x v Hx Hva) (SNo_mul_SNo u y Hua Hy) (SNo_minus_SNo (u * v) (SNo_mul_SNo u v Hua Hva)) (from left to right).
Apply HRI1 to the current goal.
An exact proof term for the current goal is Hu.
An exact proof term for the current goal is Hv.
rewrite the current goal using LLL' (from left to right).
rewrite the current goal using LRR' (from left to right).
Use reflexivity.
∎