Let alpha be given.
Assume Ha.
Let x be given.
We prove the intermediate
claim Lx:
SNo x.
An
exact proof term for the current goal is
SNo_SNo alpha Ha x Hx.
We prove the intermediate
claim Lxa:
SNoLev x = alpha.
An
exact proof term for the current goal is
SNoLev_uniq2 alpha Ha x Hx.
We prove the intermediate
claim Lmxa:
SNoLev (- x) = alpha.
rewrite the current goal using
minus_SNo_Lev x Lx (from left to right).
An exact proof term for the current goal is Lxa.
We will
prove SNo_ alpha (- x).
rewrite the current goal using Lmxa (from right to left).
∎