Definition natneqchoice (n m : nat) (ne : n ≠ m) : (n > m) ⨿ (n < m). Proof. intros. induction (natgthorleh n m) as [ l | g ]. - exact (ii1 l). - induction (natlthorgeh n m) as [ l' | g' ]. + apply (ii2 l'). + contradicts (nat_neq_to_nopath ne) (isantisymmnatleh _ _ g g'). Defined.