Let t be given.
Assume HtR: t ∈ R.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim HmmtS: SNo (minus_SNo (minus_SNo t)).
An exact proof term for the current goal is (SNo_minus_SNo (minus_SNo t) HmtS).
We prove the intermediate claim Hinv1: add_SNo (minus_SNo (minus_SNo t)) (minus_SNo t) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv (minus_SNo t) HmtS).
We prove the intermediate claim Hinv2: add_SNo t (minus_SNo t) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv t HtS).
We prove the intermediate claim Heq: add_SNo (minus_SNo (minus_SNo t)) (minus_SNo t) = add_SNo t (minus_SNo t).
rewrite the current goal using Hinv1 (from left to right).
rewrite the current goal using Hinv2 (from right to left).
Use reflexivity.
An exact proof term for the current goal is (add_SNo_cancel_R (minus_SNo (minus_SNo t)) (minus_SNo t) t HmmtS HmtS HtS Heq).
∎