N_add_succ_l@{} (n m : N) : succ n + m = succ (n + m). Proof. rewrite <- (N_add_one_r n). rewrite N_add_assoc. rewrite N_add_one_l. apply N_add_succ. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.