Let a and t be given.
Assume HaR: a ∈ R.
Assume HtR: t ∈ R.
We will prove (Rlt a (minus_SNo t) ↔ Rlt t (minus_SNo a)).
Apply iffI to the current goal.
Assume Halt: Rlt a (minus_SNo t).
We will prove Rlt t (minus_SNo a).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
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 HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim HltS: a < minus_SNo t.
An exact proof term for the current goal is (RltE_lt a (minus_SNo t) Halt).
We prove the intermediate claim HltRaw: minus_SNo (minus_SNo t) < minus_SNo a.
An exact proof term for the current goal is (minus_SNo_Lt_contra a (minus_SNo t) HaS HmtS HltS).
We prove the intermediate claim HltS2: t < minus_SNo a.
rewrite the current goal using (minus_SNo_minus_SNo_R t HtR) (from right to left) at position 1.
An exact proof term for the current goal is HltRaw.
We prove the intermediate claim HtLt: Rlt t (minus_SNo a).
We prove the intermediate claim Hm_aR: minus_SNo a ∈ R.
An exact proof term for the current goal is (real_minus_SNo a HaR).
An exact proof term for the current goal is (RltI t (minus_SNo a) HtR Hm_aR HltS2).
An exact proof term for the current goal is HtLt.
Assume Htlt: Rlt t (minus_SNo a).
We will prove Rlt a (minus_SNo t).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
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 HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
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: t < minus_SNo a.
An exact proof term for the current goal is (RltE_lt t (minus_SNo a) Htlt).
We prove the intermediate claim HltRaw: minus_SNo (minus_SNo a) < minus_SNo t.
An exact proof term for the current goal is (minus_SNo_Lt_contra t (minus_SNo a) HtS HmaS HltS).
We prove the intermediate claim HltS2: a < minus_SNo t.
rewrite the current goal using (minus_SNo_minus_SNo_R a HaR) (from right to left) at position 1.
An exact proof term for the current goal is HltRaw.
We prove the intermediate claim Hm_tR: 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 a (minus_SNo t) HaR Hm_tR HltS2).
∎