Let a, b, c and d be given.

Assume Hab: Rlt a b.

Assume Hcd: Rlt c d.

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 HcR: c ∈ R.

An exact proof term for the current goal is (RltE_left c d Hcd).

We prove the intermediate claim HdR: d ∈ R.

An exact proof term for the current goal is (RltE_right c d Hcd).

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 HcS: SNo c.

An exact proof term for the current goal is (real_SNo c HcR).

We prove the intermediate claim HdS: SNo d.

An exact proof term for the current goal is (real_SNo d HdR).

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 Hcdlt: c < d.

An exact proof term for the current goal is (RltE_lt c d Hcd).

We prove the intermediate claim Habcdlt: add_SNo a c < add_SNo b d.

An exact proof term for the current goal is (add_SNo_Lt3 a c b d HaS HcS HbS HdS Hablt Hcdlt).

We prove the intermediate claim HacR: add_SNo a c ∈ R.

An exact proof term for the current goal is (real_add_SNo a HaR c HcR).

We prove the intermediate claim HbdR: add_SNo b d ∈ R.

An exact proof term for the current goal is (real_add_SNo b HbR d HdR).

An exact proof term for the current goal is (RltI (add_SNo a c) (add_SNo b d) HacR HbdR Habcdlt).

∎