Let a, b and c be given.
Assume Hab Hbc.
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_right b c Hbc).
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 Hbclt:
b < c.
An
exact proof term for the current goal is
(RltE_lt b c Hbc).
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 Haclt:
a < c.
An
exact proof term for the current goal is
(SNoLt_tra a b c HaS HbS HcS Hablt Hbclt).
An
exact proof term for the current goal is
(RltI a c HaR HcR Haclt).