N_succ_lt@{} (n m : N) (H : n < m) : succ n < succ m. Proof. destruct H as [k H]. exists k. rewrite N_add_succ. apply ap; assumption. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.