Let t and b be given.
Assume HtR: t ∈ R.
Assume HbR: b ∈ R.
We will prove (Rlt (minus_SNo t) b ↔ Rlt (minus_SNo b) t).
Apply iffI to the current goal.
Assume Hlt: Rlt (minus_SNo t) b.
We will prove Rlt (minus_SNo b) t.
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
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 HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim HltS: minus_SNo t < b.
An exact proof term for the current goal is (RltE_lt (minus_SNo t) b Hlt).
We prove the intermediate claim Hraw: minus_SNo b < minus_SNo (minus_SNo t).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo t) b HmtS HbS HltS).
We prove the intermediate claim Hraw2: minus_SNo b < t.
rewrite the current goal using (minus_SNo_minus_SNo_R t HtR) (from right to left).
An exact proof term for the current goal is Hraw.
We prove the intermediate claim HmbR: minus_SNo b ∈ R.
An exact proof term for the current goal is (real_minus_SNo b HbR).
An exact proof term for the current goal is (RltI (minus_SNo b) t HmbR HtR Hraw2).
Assume Hlt: Rlt (minus_SNo b) t.
We will prove Rlt (minus_SNo t) b.
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
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: minus_SNo b < t.
An exact proof term for the current goal is (RltE_lt (minus_SNo b) t Hlt).
We prove the intermediate claim Hraw: minus_SNo t < minus_SNo (minus_SNo b).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo b) t HmbS HtS HltS).
We prove the intermediate claim Hraw2: minus_SNo t < b.
rewrite the current goal using (minus_SNo_minus_SNo_R b HbR) (from right to left).
An exact proof term for the current goal is Hraw.
We prove the intermediate claim HmtR: minus_SNo t ∈ R.
An exact proof term for the current goal is (real_minus_SNo t HtR).
An exact proof term for the current goal is (RltI (minus_SNo t) b HmtR HbR Hraw2).
∎