N_add_cancel_zero_r@{} (n k : N) (H : k + n = n) : k = zero. Proof. refine (N_add_cancel_r k zero n _). rewrite H; symmetry. apply path_N, graph_add_zero_l. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.