N_lt_succ@{} (n : N) : n < succ n. Proof. exists zero. rewrite N_add_succ_l. apply ap, N_add_zero_l. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.