Lemma natleh_neq {i j : nat} : i ≤ j -> i ≠ j -> i < j. Proof. intros le ne. induction (natlehchoice _ _ le) as [lt|eq]. - exact lt. - induction eq. apply fromempty. exact (isirrefl_natneq _ ne). Defined.