Let a and b be given.

Assume Hab.

Apply (RleI a b (RltE_left a b Hab) (RltE_right a b Hab)) to the current goal.

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

∎