src/HOL/Library/Nat_Infinity.thy

   "0 + (q\<Colon>inat) = q"
   "(q\<Colon>inat) + 0 = q"
   by (simp_all add: plus_inat_def zero_inat_def split: inat.splits)
 
 lemma plus_inat_number [simp]:
-  "(number_of k \<Colon> inat) + number_of l = (if neg (number_of k \<Colon> int) then number_of l
-    else if neg (number_of l \<Colon> int) then number_of k else number_of (k + l))"
+  "(number_of k \<Colon> inat) + number_of l = (if k < Int.Pls then number_of l
+    else if l < Int.Pls then number_of k else number_of (k + l))"
   unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
 
 lemma iSuc_number [simp]:
   "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
   unfolding iSuc_number_of