diff -r 817944aeac3f -r 2c38ffd6ec71 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Library/Extended_Nat.thy	Thu Feb 22 22:58:27 2018 +0000
@@ -383,6 +383,8 @@
     by (simp split: enat.splits)
   show "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" for a b c d :: enat
     by (cases a b c d rule: enat2_cases[case_product enat2_cases]) auto
+  show "a < b \<Longrightarrow> a + 1 < b + 1"
+    by (metis add_right_mono eSuc_minus_1 eSuc_plus_1 less_le)
 qed (simp add: zero_enat_def one_enat_def)
 
 (* BH: These equations are already proven generally for any type in