We will prove Rlt (minus_SNo 1) 0.

We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.

An exact proof term for the current goal is (real_minus_SNo 1 real_1).

An exact proof term for the current goal is (RltI (minus_SNo 1) 0 Hm1R real_0 minus_1_lt_0).

∎