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