{n m} : n <> m <-> (n < m) + (n > m). Proof. split. - intros diseq. destruct (dec (n < m)) as [| a]; [ by left |]. apply geq_iff_not_lt in a. apply equiv_leq_lt_or_eq in a. destruct a as [lt | eq]. 1: by right. symmetry in eq. contradiction. - intros [H' | H'] nq; destruct nq; exact (lt_irrefl _ H'). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids