N_add_one_l@{} (n : N) : one + n = succ n. Proof. revert n; refine (N_propind (fun m => one + m = succ m) _ _). - rewrite N_add_zero_r. apply path_N. symmetry; apply graph_succ_zero. - intros n H. rewrite N_add_succ. apply ap, H. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.