We prove the intermediate claim H01: 0 < 1.

An exact proof term for the current goal is SNoLt_0_1.

We prove the intermediate claim Hm1ltm0: minus_SNo 1 < minus_SNo 0.

An exact proof term for the current goal is (minus_SNo_Lt_contra 0 1 SNo_0 SNo_1 H01).

rewrite the current goal using (minus_SNo_0) (from right to left) at position 2.

An exact proof term for the current goal is Hm1ltm0.

∎