proposition: Lemma le_or_lt `{!TrivialApart A} `{DecidablePaths A} x y : x ≤ y |_| y < x.
proof: Proof. destruct (trichotomy (<) x y) as [|[|]]; try auto. - left. apply lt_le;trivial. - left. apply eq_le;trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness