Let x and y be given.
Assume Hx Hy.
We prove the intermediate
claim Lmx:
SNo (- x).
Let L and R be given.
Assume HLR HLE HLI1 HLI2 HRE HRI1 HRI2.
Let L' and R' be given.
Assume HL'R' HL'E HL'I1 HL'I2 HR'E HR'I1 HR'I2.
rewrite the current goal using Hxye (from left to right).
rewrite the current goal using L1 (from left to right).
rewrite the current goal using Hmxye (from left to right).
Use f_equal.
We will
prove L' = {- z|z ∈ R}.
Let u be given.
Let v be given.
Apply SNoL_E (- x) Lmx u Hu to the current goal.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate
claim Lmu1:
SNo (- u).
We prove the intermediate
claim Lmu2:
- u ∈ SNoR x.
Apply SNoR_I x Hx (- u) Lmu1 to the current goal.
rewrite the current goal using
minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using
minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hub.
We prove the intermediate
claim L1:
u * y + (- x) * v + - u * v = - ((- u) * y + x * v + - (- u) * v).
Use symmetry.
Use transitivity with and
- (- u) * y + - x * v + - - (- u) * v.
Use f_equal.
We will
prove - (- u) * y = u * y.
Use transitivity with and
(- - u) * y.
Use symmetry.
An
exact proof term for the current goal is
IHx (- u) (SNoR_SNoS x Hx (- u) Lmu2).
Use f_equal.
We will
prove - x * v = (- x) * v.
Use symmetry.
An
exact proof term for the current goal is
IHy v (SNoL_SNoS y Hy v Hv).
Use f_equal.
We will
prove - (- u) * v = u * v.
Use transitivity with and
(- - u) * v.
Use symmetry.
We will
prove (- - u) * v = - (- u) * v.
An
exact proof term for the current goal is
IHxy (- u) (SNoR_SNoS x Hx (- u) Lmu2) v (SNoL_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
Apply ReplI R (λz ⇒ - z) to the current goal.
We will
prove (- u) * y + x * v + - (- u) * v ∈ R.
Apply HRI2 to the current goal.
An exact proof term for the current goal is Lmu2.
We will
prove v ∈ SNoL y.
An exact proof term for the current goal is Hv.
Let u be given.
Let v be given.
Apply SNoR_E (- x) Lmx u Hu to the current goal.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate
claim Lmu1:
SNo (- u).
We prove the intermediate
claim Lmu2:
- u ∈ SNoL x.
Apply SNoL_I x Hx (- u) Lmu1 to the current goal.
rewrite the current goal using
minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using
minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hub.
We prove the intermediate
claim L1:
u * y + (- x) * v + - u * v = - ((- u) * y + x * v + - (- u) * v).
Use symmetry.
Use transitivity with and
- (- u) * y + - x * v + - - (- u) * v.
Use f_equal.
We will
prove - (- u) * y = u * y.
Use transitivity with and
(- - u) * y.
Use symmetry.
An
exact proof term for the current goal is
IHx (- u) (SNoL_SNoS x Hx (- u) Lmu2).
Use f_equal.
We will
prove - x * v = (- x) * v.
Use symmetry.
An
exact proof term for the current goal is
IHy v (SNoR_SNoS y Hy v Hv).
Use f_equal.
We will
prove - (- u) * v = u * v.
Use transitivity with and
(- - u) * v.
Use symmetry.
We will
prove (- - u) * v = - (- u) * v.
An
exact proof term for the current goal is
IHxy (- u) (SNoL_SNoS x Hx (- u) Lmu2) v (SNoR_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
Apply ReplI R (λz ⇒ - z) to the current goal.
We will
prove (- u) * y + x * v + - (- u) * v ∈ R.
Apply HRI1 to the current goal.
An exact proof term for the current goal is Lmu2.
We will
prove v ∈ SNoR y.
An exact proof term for the current goal is Hv.
We will
prove {- z|z ∈ R} ⊆ L'.
Let a be given.
Assume Ha.
Let z be given.
rewrite the current goal using Hze (from left to right).
Apply HRE z Hz to the current goal.
Let u be given.
Let v be given.
Apply SNoL_E x Hx u Hu to the current goal.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate
claim Lmu1:
SNo (- u).
We prove the intermediate
claim Lmu2:
- u ∈ SNoR (- x).
rewrite the current goal using
minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using
minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hub.
We prove the intermediate
claim L1:
- z = (- u) * y + (- x) * v + - (- u) * v.
rewrite the current goal using Hzuv (from left to right).
Use f_equal.
We will
prove - (u * y) = (- u) * y.
Use symmetry.
An
exact proof term for the current goal is
IHx u (SNoL_SNoS x Hx u Hu).
Use f_equal.
We will
prove - (x * v) = (- x) * v.
Use symmetry.
An
exact proof term for the current goal is
IHy v (SNoR_SNoS y Hy v Hv).
Use f_equal.
We will
prove - (u * v) = (- u) * v.
Use symmetry.
An
exact proof term for the current goal is
IHxy u (SNoL_SNoS x Hx u Hu) v (SNoR_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
We will
prove (- u) * y + (- x) * v + - (- u) * v ∈ L'.
Apply HL'I2 to the current goal.
An exact proof term for the current goal is Lmu2.
An exact proof term for the current goal is Hv.
Let u be given.
Let v be given.
Apply SNoR_E x Hx u Hu to the current goal.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate
claim Lmu1:
SNo (- u).
We prove the intermediate
claim Lmu2:
- u ∈ SNoL (- x).
rewrite the current goal using
minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using
minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hub.
We prove the intermediate
claim L1:
- z = (- u) * y + (- x) * v + - (- u) * v.
rewrite the current goal using Hzuv (from left to right).
Use f_equal.
We will
prove - (u * y) = (- u) * y.
Use symmetry.
An
exact proof term for the current goal is
IHx u (SNoR_SNoS x Hx u Hu).
Use f_equal.
We will
prove - (x * v) = (- x) * v.
Use symmetry.
An
exact proof term for the current goal is
IHy v (SNoL_SNoS y Hy v Hv).
Use f_equal.
We will
prove - (u * v) = (- u) * v.
Use symmetry.
An
exact proof term for the current goal is
IHxy u (SNoR_SNoS x Hx u Hu) v (SNoL_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
We will
prove (- u) * y + (- x) * v + - (- u) * v ∈ L'.
Apply HL'I1 to the current goal.
An exact proof term for the current goal is Lmu2.
An exact proof term for the current goal is Hv.
We will
prove R' = {- w|w ∈ L}.
Let u be given.
Let v be given.
Apply SNoL_E (- x) Lmx u Hu to the current goal.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate
claim Lmu1:
SNo (- u).
We prove the intermediate
claim Lmu2:
- u ∈ SNoR x.
Apply SNoR_I x Hx (- u) Lmu1 to the current goal.
rewrite the current goal using
minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using
minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hub.
We prove the intermediate
claim L1:
u * y + (- x) * v + - u * v = - ((- u) * y + x * v + - (- u) * v).
Use symmetry.
Use transitivity with and
- (- u) * y + - x * v + - - (- u) * v.
Use f_equal.
We will
prove - (- u) * y = u * y.
Use transitivity with and
(- - u) * y.
Use symmetry.
An
exact proof term for the current goal is
IHx (- u) (SNoR_SNoS x Hx (- u) Lmu2).
Use f_equal.
We will
prove - x * v = (- x) * v.
Use symmetry.
An
exact proof term for the current goal is
IHy v (SNoR_SNoS y Hy v Hv).
Use f_equal.
We will
prove - (- u) * v = u * v.
Use transitivity with and
(- - u) * v.
Use symmetry.
We will
prove (- - u) * v = - (- u) * v.
An
exact proof term for the current goal is
IHxy (- u) (SNoR_SNoS x Hx (- u) Lmu2) v (SNoR_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
Apply ReplI L (λw ⇒ - w) to the current goal.
We will
prove (- u) * y + x * v + - (- u) * v ∈ L.
Apply HLI2 to the current goal.
An exact proof term for the current goal is Lmu2.
We will
prove v ∈ SNoR y.
An exact proof term for the current goal is Hv.
Let u be given.
Let v be given.
Apply SNoR_E (- x) Lmx u Hu to the current goal.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate
claim Lmu1:
SNo (- u).
We prove the intermediate
claim Lmu2:
- u ∈ SNoL x.
Apply SNoL_I x Hx (- u) Lmu1 to the current goal.
rewrite the current goal using
minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using
minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hub.
We prove the intermediate
claim L1:
u * y + (- x) * v + - u * v = - ((- u) * y + x * v + - (- u) * v).
Use symmetry.
Use transitivity with and
- (- u) * y + - x * v + - - (- u) * v.
Use f_equal.
We will
prove - (- u) * y = u * y.
Use transitivity with and
(- - u) * y.
Use symmetry.
An
exact proof term for the current goal is
IHx (- u) (SNoL_SNoS x Hx (- u) Lmu2).
Use f_equal.
We will
prove - x * v = (- x) * v.
Use symmetry.
An
exact proof term for the current goal is
IHy v (SNoL_SNoS y Hy v Hv).
Use f_equal.
We will
prove - (- u) * v = u * v.
Use transitivity with and
(- - u) * v.
Use symmetry.
We will
prove (- - u) * v = - (- u) * v.
An
exact proof term for the current goal is
IHxy (- u) (SNoL_SNoS x Hx (- u) Lmu2) v (SNoL_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
Apply ReplI L (λw ⇒ - w) to the current goal.
We will
prove (- u) * y + x * v + - (- u) * v ∈ L.
Apply HLI1 to the current goal.
An exact proof term for the current goal is Lmu2.
We will
prove v ∈ SNoL y.
An exact proof term for the current goal is Hv.
We will
prove {- w|w ∈ L} ⊆ R'.
Let a be given.
Assume Ha.
Let w be given.
rewrite the current goal using Hwe (from left to right).
Apply HLE w Hw to the current goal.
Let u be given.
Let v be given.
Apply SNoL_E x Hx u Hu to the current goal.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate
claim Lmu1:
SNo (- u).
We prove the intermediate
claim Lmu2:
- u ∈ SNoR (- x).
rewrite the current goal using
minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using
minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hub.
We prove the intermediate
claim L1:
- w = (- u) * y + (- x) * v + - (- u) * v.
rewrite the current goal using Hwuv (from left to right).
Use f_equal.
We will
prove - (u * y) = (- u) * y.
Use symmetry.
An
exact proof term for the current goal is
IHx u (SNoL_SNoS x Hx u Hu).
Use f_equal.
We will
prove - (x * v) = (- x) * v.
Use symmetry.
An
exact proof term for the current goal is
IHy v (SNoL_SNoS y Hy v Hv).
Use f_equal.
We will
prove - (u * v) = (- u) * v.
Use symmetry.
An
exact proof term for the current goal is
IHxy u (SNoL_SNoS x Hx u Hu) v (SNoL_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
We will
prove (- u) * y + (- x) * v + - (- u) * v ∈ R'.
Apply HR'I2 to the current goal.
An exact proof term for the current goal is Lmu2.
An exact proof term for the current goal is Hv.
Let u be given.
Let v be given.
Apply SNoR_E x Hx u Hu to the current goal.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hva _ _.
We prove the intermediate
claim Lmu1:
SNo (- u).
We prove the intermediate
claim Lmu2:
- u ∈ SNoL (- x).
rewrite the current goal using
minus_SNo_Lev u Hua (from left to right).
rewrite the current goal using
minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hub.
We prove the intermediate
claim L1:
- w = (- u) * y + (- x) * v + - (- u) * v.
rewrite the current goal using Hwuv (from left to right).
Use f_equal.
We will
prove - (u * y) = (- u) * y.
Use symmetry.
An
exact proof term for the current goal is
IHx u (SNoR_SNoS x Hx u Hu).
Use f_equal.
We will
prove - (x * v) = (- x) * v.
Use symmetry.
An
exact proof term for the current goal is
IHy v (SNoR_SNoS y Hy v Hv).
Use f_equal.
We will
prove - (u * v) = (- u) * v.
Use symmetry.
An
exact proof term for the current goal is
IHxy u (SNoR_SNoS x Hx u Hu) v (SNoR_SNoS y Hy v Hv).
rewrite the current goal using L1 (from left to right).
We will
prove (- u) * y + (- x) * v + - (- u) * v ∈ R'.
Apply HR'I1 to the current goal.
An exact proof term for the current goal is Lmu2.
An exact proof term for the current goal is Hv.
∎