Let a, b and c be given.
Assume HaS: SNo a.
Assume HbS: SNo b.
Assume HcS: SNo c.
Set x to be the term add_SNo a (minus_SNo b).
Set y to be the term add_SNo b (minus_SNo c).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim HmcS: SNo (minus_SNo c).
An exact proof term for the current goal is (SNo_minus_SNo c HcS).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (SNo_add_SNo a (minus_SNo b) HaS HmbS).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (SNo_add_SNo b (minus_SNo c) HbS HmcS).
We prove the intermediate claim HxyS: SNo (add_SNo x y).
An exact proof term for the current goal is (SNo_add_SNo x y HxS HyS).
We prove the intermediate claim HrhsS: SNo (add_SNo (abs_SNo x) (abs_SNo y)).
An exact proof term for the current goal is (SNo_add_SNo (abs_SNo x) (abs_SNo y) (SNo_abs_SNo x HxS) (SNo_abs_SNo y HyS)).
We prove the intermediate claim Hsum: add_SNo x y = add_SNo a (minus_SNo c).
We prove the intermediate claim Hassoc1: add_SNo x y = add_SNo (add_SNo a (minus_SNo b)) (add_SNo b (minus_SNo c)).
Use reflexivity.
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using (add_SNo_assoc a (minus_SNo b) (add_SNo b (minus_SNo c)) HaS HmbS (SNo_add_SNo b (minus_SNo c) HbS HmcS)) (from right to left).
rewrite the current goal using (add_SNo_assoc (minus_SNo b) b (minus_SNo c) HmbS HbS HmcS) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_linv b HbS) (from left to right).
rewrite the current goal using (add_SNo_0L (minus_SNo c) HmcS) (from left to right).
Use reflexivity.
rewrite the current goal using Hsum (from right to left) at position 1.
An exact proof term for the current goal is (abs_SNo_subadd x y HxS HyS).
∎