N_add_assoc@{} (n m k : N) : (n + m) + k = n + (m + k). Proof. apply path_N, graph_add_assoc. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.