Let a and b be given.
Assume Hab: Rlt a b.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (RltE_left a b Hab).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (RltE_right a b Hab).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim Hablt: a < b.
An exact proof term for the current goal is (RltE_lt a b Hab).
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 Hmablt: add_SNo (minus_SNo a) a < add_SNo (minus_SNo a) b.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo a) a b HmaS HaS HbS Hablt).
We prove the intermediate claim H0lt: 0 < add_SNo (minus_SNo a) b.
rewrite the current goal using (add_SNo_minus_SNo_linv a HaS) (from right to left) at position 1.
An exact proof term for the current goal is Hmablt.
We prove the intermediate claim HmabR: add_SNo (minus_SNo a) b ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo a) (real_minus_SNo a HaR) b HbR).
We prove the intermediate claim Hcom: add_SNo (minus_SNo a) b = add_SNo b (minus_SNo a).
An exact proof term for the current goal is (add_SNo_com (minus_SNo a) b HmaS HbS).
We prove the intermediate claim HbaR: add_SNo b (minus_SNo a) ∈ R.
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo a) (real_minus_SNo a HaR)).
We prove the intermediate claim H0lt2: 0 < add_SNo b (minus_SNo a).
rewrite the current goal using Hcom (from right to left).
An exact proof term for the current goal is H0lt.
An exact proof term for the current goal is (RltI 0 (add_SNo b (minus_SNo a)) real_0 HbaR H0lt2).
∎