N_succ_nlt@{} (n : N) : ~(succ n < n). Proof. revert n; apply N_propind@{p}. - intros n;exact istrunc_arrow@{p p p}. - apply N_lt_zero. - intros n H L. apply H; clear H. destruct L as [k H]. exists k. rewrite N_add_succ in H. exact (succ_inj _ _ H). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.