Let a be given.

Assume Ha.

Apply (RleI a a Ha Ha) to the current goal.

An exact proof term for the current goal is (not_Rlt_refl a Ha).

∎