`{!TrivialApart A} `{forall x y, Decidable (x ≤ y)} : forall x y, Decidable (x < y). Proof. intros. destruct (decide_rel (<=) y x). - right;apply le_not_lt_flip;assumption. - left; apply not_le_lt_flip;assumption. Defined.
Require Import