--- 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)