Set P to be the term λx y z ⇒ x * (y * z) = (x * y) * z of type set → set → set → prop.
We will prove ∀x y z, SNo x → SNo y → SNo z → P x y z.
Apply SNoLev_ind3 P to the current goal.
Let x, y and z be given.
Assume Hx Hy Hz.
Assume IHx: ∀u ∈ SNoS_ (SNoLev x), u * (y * z) = (u * y) * z.
Assume IHy: ∀v ∈ SNoS_ (SNoLev y), x * (v * z) = (x * v) * z.
Assume IHz: ∀w ∈ SNoS_ (SNoLev z), x * (y * w) = (x * y) * w.
Assume IHxy: ∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), u * (v * z) = (u * v) * z.
Assume IHxz: ∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), u * (y * w) = (u * y) * w.
Assume IHyz: ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), x * (v * w) = (x * v) * w.
Assume IHxyz: ∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), u * (v * w) = (u * v) * w.
We will prove x * (y * z) = (x * y) * z.
We prove the intermediate claim Lxy: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Hx Hy.
We prove the intermediate claim Lyz: SNo (y * z).
An exact proof term for the current goal is SNo_mul_SNo y z Hy Hz.
We prove the intermediate claim Lxyz1: SNo (x * (y * z)).
An exact proof term for the current goal is SNo_mul_SNo x (y * z) Hx Lyz.
We prove the intermediate claim Lxyz2: SNo ((x * y) * z).
An exact proof term for the current goal is SNo_mul_SNo (x * y) z Lxy Hz.
Apply mul_SNo_eq_3 x (y * z) Hx Lyz to the current goal.
Let L and R be given.
Assume HLR HLE HLI1 HLI2 HRE HRI1 HRI2.
Assume HE: x * (y * z) = SNoCut L R.
Apply mul_SNo_eq_3 (x * y) z Lxy Hz to the current goal.
Let L' and R' be given.
Assume HLR' HLE' HLI1' HLI2' HRE' HRI1' HRI2'.
Assume HE': (x * y) * z = SNoCut L' R'.
rewrite the current goal using HE (from left to right).
rewrite the current goal using HE' (from left to right).
We will prove SNoCut L R = SNoCut L' R'.
We prove the intermediate claim LIL': ∀x y, SNo x → SNo y → ∀u ∈ SNoL (y * x), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL y, u + w * v ≤ y * v + w * x → p) → (∀v ∈ SNoR x, ∀w ∈ SNoR y, u + w * v ≤ y * v + w * x → p) → p.
Let x and y be given.
Assume Hx Hy.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp1 Hp2.
Apply mul_SNo_SNoL_interpolate_impred y x Hy Hx u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL y.
Let v be given.
Assume Hv: v ∈ SNoL x.
Apply SNoL_E y Hy w Hw to the current goal.
Assume Hw1 _ _.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1 _ _.
We will prove u + w * v ≤ w * x + y * v → p.
rewrite the current goal using add_SNo_com (w * x) (y * v) (SNo_mul_SNo w x Hw1 Hx) (SNo_mul_SNo y v Hy Hv1) (from left to right).
An exact proof term for the current goal is Hp1 v Hv w Hw.
Let w be given.
Assume Hw: w ∈ SNoR y.
Let v be given.
Assume Hv: v ∈ SNoR x.
Apply SNoR_E y Hy w Hw to the current goal.
Assume Hw1 _ _.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1 _ _.
We will prove u + w * v ≤ w * x + y * v → p.
rewrite the current goal using add_SNo_com (w * x) (y * v) (SNo_mul_SNo w x Hw1 Hx) (SNo_mul_SNo y v Hy Hv1) (from left to right).
An exact proof term for the current goal is Hp2 v Hv w Hw.
We prove the intermediate claim LIR': ∀x y, SNo x → SNo y → ∀u ∈ SNoR (y * x), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR y, y * v + w * x ≤ u + w * v → p) → (∀v ∈ SNoR x, ∀w ∈ SNoL y, y * v + w * x ≤ u + w * v → p) → p.
Let x and y be given.
Assume Hx Hy.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp1 Hp2.
Apply mul_SNo_SNoR_interpolate_impred y x Hy Hx u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL y.
Let v be given.
Assume Hv: v ∈ SNoR x.
Apply SNoL_E y Hy w Hw to the current goal.
Assume Hw1 _ _.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1 _ _.
rewrite the current goal using add_SNo_com (w * x) (y * v) (SNo_mul_SNo w x Hw1 Hx) (SNo_mul_SNo y v Hy Hv1) (from left to right).
An exact proof term for the current goal is Hp2 v Hv w Hw.
Let w be given.
Assume Hw: w ∈ SNoR y.
Let v be given.
Assume Hv: v ∈ SNoL x.
Apply SNoR_E y Hy w Hw to the current goal.
Assume Hw1 _ _.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1 _ _.
rewrite the current goal using add_SNo_com (w * x) (y * v) (SNo_mul_SNo w x Hw1 Hx) (SNo_mul_SNo y v Hy Hv1) (from left to right).
An exact proof term for the current goal is Hp1 v Hv w Hw.
We prove the intermediate claim LMLt': ∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → y * u + v * x < y * x + v * u.
Let x, y, u and v be given.
Assume Hx Hy Hu Hv Hux Hvy.
rewrite the current goal using add_SNo_com (y * u) (v * x) (SNo_mul_SNo y u Hy Hu) (SNo_mul_SNo v x Hv Hx) (from left to right).
We will prove v * x + y * u < y * x + v * u.
An exact proof term for the current goal is mul_SNo_Lt y x v u Hy Hx Hv Hu Hvy Hux.
We prove the intermediate claim LMLe': ∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → y * u + v * x ≤ y * x + v * u.
Let x, y, u and v be given.
Assume Hx Hy Hu Hv Hux Hvy.
rewrite the current goal using add_SNo_com (y * u) (v * x) (SNo_mul_SNo y u Hy Hu) (SNo_mul_SNo v x Hv Hx) (from left to right).
We will prove v * x + y * u ≤ y * x + v * u.
An exact proof term for the current goal is mul_SNo_Le y x v u Hy Hx Hv Hu Hvy Hux.
We prove the intermediate claim LIHx': ∀u ∈ SNoS_ (SNoLev x), (u * y) * z = u * (y * z).
Let u be given.
Assume Hu.
Use symmetry.
An exact proof term for the current goal is IHx u Hu.
We prove the intermediate claim LIHy': ∀v ∈ SNoS_ (SNoLev y), (x * v) * z = x * (v * z).
Let v be given.
Assume Hv.
Use symmetry.
An exact proof term for the current goal is IHy v Hv.
We prove the intermediate claim LIHz': ∀w ∈ SNoS_ (SNoLev z), (x * y) * w = x * (y * w).
Let w be given.
Assume Hw.
Use symmetry.
An exact proof term for the current goal is IHz w Hw.
We prove the intermediate claim LIHyx': ∀v ∈ SNoS_ (SNoLev y), ∀u ∈ SNoS_ (SNoLev x), (u * v) * z = u * (v * z).
Let v be given.
Assume Hv.
Let u be given.
Assume Hu.
Use symmetry.
An exact proof term for the current goal is IHxy u Hu v Hv.
We prove the intermediate claim LIHzx': ∀w ∈ SNoS_ (SNoLev z), ∀u ∈ SNoS_ (SNoLev x), (u * y) * w = u * (y * w).
Let w be given.
Assume Hw.
Let u be given.
Assume Hu.
Use symmetry.
An exact proof term for the current goal is IHxz u Hu w Hw.
We prove the intermediate claim LIHzy': ∀w ∈ SNoS_ (SNoLev z), ∀v ∈ SNoS_ (SNoLev y), (x * v) * w = x * (v * w).
Let w be given.
Assume Hw.
Let v be given.
Assume Hv.
Use symmetry.
An exact proof term for the current goal is IHyz v Hv w Hw.
We prove the intermediate claim LIHzyx': ∀w ∈ SNoS_ (SNoLev z), ∀v ∈ SNoS_ (SNoLev y), ∀u ∈ SNoS_ (SNoLev x), (u * v) * w = u * (v * w).
Let w be given.
Assume Hw.
Let v be given.
Assume Hv.
Let u be given.
Assume Hu.
Use symmetry.
An exact proof term for the current goal is IHxyz u Hu v Hv w Hw.
Apply SNoCut_ext to the current goal.
An exact proof term for the current goal is HLR.
An exact proof term for the current goal is HLR'.
rewrite the current goal using HE' (from right to left).
We will prove ∀u ∈ L, u < (x * y) * z.
An exact proof term for the current goal is mul_SNo_assoc_lem1 mul_SNo SNo_mul_SNo mul_SNo_distrL mul_SNo_distrR mul_SNo_SNoL_interpolate_impred mul_SNo_SNoR_interpolate_impred mul_SNo_Lt mul_SNo_Le x y z Hx Hy Hz IHx IHy IHz IHxy IHxz IHyz IHxyz L HLE.
rewrite the current goal using HE' (from right to left).
We will prove ∀u ∈ R, (x * y) * z < u.
An exact proof term for the current goal is mul_SNo_assoc_lem2 mul_SNo SNo_mul_SNo mul_SNo_distrL mul_SNo_distrR mul_SNo_SNoL_interpolate_impred mul_SNo_SNoR_interpolate_impred mul_SNo_Lt mul_SNo_Le x y z Hx Hy Hz IHx IHy IHz IHxy IHxz IHyz IHxyz R HRE.
rewrite the current goal using HE (from right to left).
We will prove ∀u ∈ L', u < x * (y * z).
Apply mul_SNo_assoc_lem1 (λx y ⇒ y * x) (λx y Hx Hy ⇒ SNo_mul_SNo y x Hy Hx) (λx y z Hx Hy Hz ⇒ mul_SNo_distrR y z x Hy Hz Hx) (λx y z Hx Hy Hz ⇒ mul_SNo_distrL z x y Hz Hx Hy) LIL' LIR' LMLt' LMLe' z y x Hz Hy Hx LIHz' LIHy' LIHx' LIHzy' LIHzx' LIHyx' LIHzyx' to the current goal.
We will prove ∀u ∈ L', ∀q : prop, (∀v ∈ SNoL z, ∀w ∈ SNoL (x * y), u = (x * y) * v + w * z + - w * v → q) → (∀v ∈ SNoR z, ∀w ∈ SNoR (x * y), u = (x * y) * v + w * z + - w * v → q) → q.
Let u be given.
Assume Hu.
Let q be given.
Assume Hq1 Hq2.
Apply HLE' u Hu to the current goal.
Let w be given.
Assume Hw.
Let v be given.
Assume Hv.
Apply SNoL_E (x * y) Lxy w Hw to the current goal.
Assume Hw1 _ _.
Apply SNoL_E z Hz v Hv to the current goal.
Assume Hv1 _ _.
We will prove u = w * z + (x * y) * v + - w * v → q.
rewrite the current goal using add_SNo_com_3_0_1 (w * z) ((x * y) * v) (- w * v) (SNo_mul_SNo w z Hw1 Hz) (SNo_mul_SNo (x * y) v Lxy Hv1) (SNo_minus_SNo (w * v) (SNo_mul_SNo w v Hw1 Hv1)) (from left to right).
An exact proof term for the current goal is Hq1 v Hv w Hw.
Let w be given.
Assume Hw.
Let v be given.
Assume Hv.
Apply SNoR_E (x * y) Lxy w Hw to the current goal.
Assume Hw1 _ _.
Apply SNoR_E z Hz v Hv to the current goal.
Assume Hv1 _ _.
We will prove u = w * z + (x * y) * v + - w * v → q.
rewrite the current goal using add_SNo_com_3_0_1 (w * z) ((x * y) * v) (- w * v) (SNo_mul_SNo w z Hw1 Hz) (SNo_mul_SNo (x * y) v Lxy Hv1) (SNo_minus_SNo (w * v) (SNo_mul_SNo w v Hw1 Hv1)) (from left to right).
An exact proof term for the current goal is Hq2 v Hv w Hw.
rewrite the current goal using HE (from right to left).
We will prove ∀u ∈ R', x * (y * z) < u.
Apply mul_SNo_assoc_lem2 (λx y ⇒ y * x) (λx y Hx Hy ⇒ SNo_mul_SNo y x Hy Hx) (λx y z Hx Hy Hz ⇒ mul_SNo_distrR y z x Hy Hz Hx) (λx y z Hx Hy Hz ⇒ mul_SNo_distrL z x y Hz Hx Hy) LIL' LIR' LMLt' LMLe' z y x Hz Hy Hx LIHz' LIHy' LIHx' LIHzy' LIHzx' LIHyx' LIHzyx' to the current goal.
We will prove ∀u ∈ R', ∀q : prop, (∀v ∈ SNoL z, ∀w ∈ SNoR (x * y), u = (x * y) * v + w * z + - w * v → q) → (∀v ∈ SNoR z, ∀w ∈ SNoL (x * y), u = (x * y) * v + w * z + - w * v → q) → q.
Let u be given.
Assume Hu.
Let q be given.
Assume Hq1 Hq2.
Apply HRE' u Hu to the current goal.
Let w be given.
Assume Hw.
Let v be given.
Assume Hv.
Apply SNoL_E (x * y) Lxy w Hw to the current goal.
Assume Hw1 _ _.
Apply SNoR_E z Hz v Hv to the current goal.
Assume Hv1 _ _.
We will prove u = w * z + (x * y) * v + - w * v → q.
rewrite the current goal using add_SNo_com_3_0_1 (w * z) ((x * y) * v) (- w * v) (SNo_mul_SNo w z Hw1 Hz) (SNo_mul_SNo (x * y) v Lxy Hv1) (SNo_minus_SNo (w * v) (SNo_mul_SNo w v Hw1 Hv1)) (from left to right).
An exact proof term for the current goal is Hq2 v Hv w Hw.
Let w be given.
Assume Hw.
Let v be given.
Assume Hv.
Apply SNoR_E (x * y) Lxy w Hw to the current goal.
Assume Hw1 _ _.
Apply SNoL_E z Hz v Hv to the current goal.
Assume Hv1 _ _.
We will prove u = w * z + (x * y) * v + - w * v → q.
rewrite the current goal using add_SNo_com_3_0_1 (w * z) ((x * y) * v) (- w * v) (SNo_mul_SNo w z Hw1 Hz) (SNo_mul_SNo (x * y) v Lxy Hv1) (SNo_minus_SNo (w * v) (SNo_mul_SNo w v Hw1 Hv1)) (from left to right).
An exact proof term for the current goal is Hq1 v Hv w Hw.
∎