N_lt_irref@{} (n : N) : ~(n < n). Proof. revert n; apply N_propind@{p}. - intros n;exact istrunc_arrow@{p p p}. - apply N_lt_zero. - intros n H [k K]. apply H; exists k. rewrite N_add_succ in K. apply succ_inj; assumption. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.