Let x, y and z be given.
Assume Hx Hy Hz.
We prove the intermediate
claim Lmy:
SNo (- y).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hy.
We prove the intermediate
claim Lmz:
SNo (- z).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hz.
We prove the intermediate
claim L1:
x + - z = (x + - y) + (y + - z).
rewrite the current goal using
add_SNo_assoc x (- y) (y + - z) Hx Lmy (SNo_add_SNo y (- z) Hy Lmz) (from right to left).
We will
prove x + - z = x + (- y + y + - z).
Use f_equal.
Use symmetry.
An
exact proof term for the current goal is
add_SNo_minus_L2 y (- z) Hy Lmz.
rewrite the current goal using L1 (from left to right).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Lmy.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Lmz.