Let x and y be given.
Assume Hx Hy.
We prove the intermediate claim Lmx: SNo (- x).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
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 Lymx: SNo (y + - x).
An exact proof term for the current goal is SNo_add_SNo y (- x) Hy Lmx.
Use transitivity with and abs_SNo (- (y + - x)).
Use f_equal.
We will prove x + - y = - (y + - x).
rewrite the current goal using minus_add_SNo_distr y (- x) Hy Lmx (from left to right).
We will prove x + - y = - y + - - x.
rewrite the current goal using minus_SNo_invol x Hx (from left to right).
We will prove x + - y = - y + x.
An exact proof term for the current goal is add_SNo_com x (- y) Hx Lmy.
An exact proof term for the current goal is abs_SNo_minus (y + - x) Lymx.
∎