Let a and b be given.

Assume Hab.

Assume Hba.

We prove the intermediate claim Haa: Rlt a a.

An exact proof term for the current goal is (Rlt_tra a b a Hab Hba).

An exact proof term for the current goal is (not_Rlt_refl a (RltE_left a b Hab) Haa).

∎