# HG changeset patch
# User nipkow
# Date 1550020426 -3600
# Node ID 74c1a0643010fab3db297c2895ee5057fa29beec
# Parent  18cb541a975f6f4ef60f8586d8c569cc0b34e01a
added lemmas

diff -r 18cb541a975f -r 74c1a0643010 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Sun Feb 10 22:24:22 2019 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Wed Feb 13 02:13:46 2019 +0100
@@ -392,6 +392,9 @@
 it does not have the cancellation property. Would it be worthwhile to
 a generalize linordered_semidom to a new class that includes enat? *)
 
+lemma add_diff_assoc_enat: "z \<le> y \<Longrightarrow> x + (y - z) = x + y - (z::enat)"
+by(cases x)(auto simp add: diff_enat_def split: enat.split)
+
 lemma enat_ord_number [simp]:
   "(numeral m :: enat) \<le> numeral n \<longleftrightarrow> (numeral m :: nat) \<le> numeral n"
   "(numeral m :: enat) < numeral n \<longleftrightarrow> (numeral m :: nat) < numeral n"
@@ -528,6 +531,9 @@
 lemma enat_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::enat) \<and> b < c"
   unfolding plus_enat_def by (simp split: enat.split)
 
+lemma plus_eq_infty_iff_enat[simp]: "(m::enat) + n = \<infinity> \<longleftrightarrow> m=\<infinity> \<or> n=\<infinity>"
+using enat_add_left_cancel by fastforce
+
 ML \<open>
 structure Cancel_Enat_Common =
 struct