include "ground/arith/nat.ma".
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
definition nsucc: nat → nat ≝ λm. match m with
[ nzero ⇒ ninj (𝟏)
#m #IH #n elim n -n /2 width=1 by/
qed-.
-(* Basic inversions *********************************************************)
+(* Basic inversions ***************************************************************)
(*** injective_S *)
lemma eq_inv_nsucc_bi: injective … nsucc.