`{!TrivialApart A} `{forall x y, Decidable (x ≤ y)} : DecidablePaths A. Proof. intros x y. destruct (decide_rel (<=) x y) as [E1|E1]; [destruct (decide_rel (<=) y x) as [E2|E2]|]. - left. apply (antisymmetry (<=));assumption. - right. intros E3;apply E2. pattern y. apply (transport _ E3). apply reflexivity. - right. intros E3;apply E1. pattern y; apply (transport _ E3). apply reflexivity. Defined.
Require Import