N_neq_succ@{} (n : N) : n <> succ n. Proof. revert n; apply N_propind@{p}. - intros n;exact istrunc_arrow@{p p p}. - apply zero_neq_succ. - intros n H e. apply H. exact (succ_inj n (succ n) e). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.