Apply add_SNo_cancel_L 0 (- 0) 0 SNo_0 (SNo_minus_SNo 0 SNo_0) SNo_0 to the current goal.

We will prove 0 + - 0 = 0 + 0.

Use transitivity with and 0.

An exact proof term for the current goal is add_SNo_minus_SNo_rinv 0 SNo_0.

Use symmetry.

An exact proof term for the current goal is add_SNo_0L 0 SNo_0.

∎