diff -r 6ec272e153f0 -r a24865b6262f src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Wed Feb 13 09:50:16 2019 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Wed Feb 13 11:25:23 2019 +0100
@@ -522,6 +522,9 @@
 
 subsection \<open>Cancellation simprocs\<close>
 
+lemma add_diff_cancel_enat[simp]: "x \<noteq> \<infinity> \<Longrightarrow> x + y - x = (y::enat)"
+by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl)
+
 lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c"
   unfolding plus_enat_def by (simp split: enat.split)