added lemma
authornipkow
Wed Feb 13 11:25:23 2019 +0100 (2 months ago)
changeset 69803a24865b6262f
parent 69802 6ec272e153f0
child 69804 9efccbad7d42
added lemma
src/HOL/Library/Extended_Nat.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Wed Feb 13 09:50:16 2019 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Feb 13 11:25:23 2019 +0100
     1.3 @@ -522,6 +522,9 @@
     1.4  
     1.5  subsection \<open>Cancellation simprocs\<close>
     1.6  
     1.7 +lemma add_diff_cancel_enat[simp]: "x \<noteq> \<infinity> \<Longrightarrow> x + y - x = (y::enat)"
     1.8 +by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl)
     1.9 +
    1.10  lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c"
    1.11    unfolding plus_enat_def by (simp split: enat.split)
    1.12