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 .
Let x, y and z be given.
Assume Hx Hy Hz .
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 .
Let L and R be given.
Assume HLR HLE HLI1 HLI2 HRE HRI1 HRI2 .
Let L' and R' be given.
Assume HLR' HLE' HLI1' HLI2' HRE' HRI1' HRI2' .
rewrite the current goal using HE (from left to right).
rewrite the current goal using HE' (from left to right).
Let x and y be given.
Assume Hx Hy .
Let u be given.
Assume Hu .
Let p be given.
Assume Hp1 Hp2 .
Let w be given.
Let v be given.
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 .
An exact proof term for the current goal is Hp1 v Hv w Hw .
Let w be given.
Let v be given.
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 .
An exact proof term for the current goal is Hp2 v Hv w Hw .
Let x and y be given.
Assume Hx Hy .
Let u be given.
Assume Hu .
Let p be given.
Assume Hp1 Hp2 .
Let w be given.
Let v be given.
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 _ _ .
An exact proof term for the current goal is Hp2 v Hv w Hw .
Let w be given.
Let v be given.
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 _ _ .
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 .
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 .
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 .
Let u be given.
Assume Hu .
Use symmetry.
An exact proof term for the current goal is IHx u Hu .
Let v be given.
Assume Hv .
Use symmetry.
An exact proof term for the current goal is IHy v Hv .
Let w be given.
Assume Hw .
Use symmetry.
An exact proof term for the current goal is IHz w Hw .
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 .
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 .
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 .
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 .
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 .
rewrite the current goal using HE' (from right to left).
We will
prove ∀ u ∈ R , (x * y ) * z < u .
rewrite the current goal using HE (from right to left).
We will
prove ∀ u ∈ L' , u < x * (y * z ) .
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 .
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 .
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 .
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 .
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 .
An exact proof term for the current goal is Hq1 v Hv w Hw .
∎