N_add_cancel_r@{} (n m k : N) (H : n + k = m + k) : n = m. Proof. revert k H. refine (N_propind _ _ _). - intros H; rewrite !N_add_zero_r in H; exact H. - intros k H1 H2. rewrite !N_add_succ in H2. apply H1. exact (succ_inj _ _ H2). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.