`{!TrivialApart A} `{forall x y, Decidable (x ≤ y)} : forall x y, Decidable (x < y). Proof. intros x y. destruct (dec (x ≤ y)); [destruct (dec (x = y))|]. - right. apply eq_not_lt. assumption. - left. apply lt_iff_le_ne. auto. - right. apply not_le_not_lt. assumption. Defined.
Require Import