Let t be given.
Assume HtR: t ∈ R.
Assume Hnlt: ¬ (Rlt t 0).
We will prove Rle (minus_SNo t) 0.
Apply (RleI (minus_SNo t) 0 (real_minus_SNo t HtR) real_0) to the current goal.
Assume Hlt: Rlt 0 (minus_SNo t).
We will prove False.
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 HltS: 0 < minus_SNo t.
An exact proof term for the current goal is (andER (0 ∈ R ∧ minus_SNo t ∈ R) (0 < minus_SNo t) Hlt).
We prove the intermediate claim Hflip: minus_SNo (minus_SNo t) < minus_SNo 0.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 (minus_SNo t) SNo_0 HmtS HltS).
We prove the intermediate claim Htlt0: t < 0.
rewrite the current goal using (minus_SNo_invol t HtS) (from right to left) at position 1.
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Hflip.
We prove the intermediate claim Hbad: Rlt t 0.
We will prove t ∈ R ∧ 0 ∈ R ∧ t < 0.
Apply and3I to the current goal.
An exact proof term for the current goal is HtR.
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is Htlt0.
An exact proof term for the current goal is (Hnlt Hbad).
∎