N_add_one_r@{} (n : N) : n + one = succ n. Proof. apply path_N; cbn. apply graph_add_one_succ. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.