equal
deleted
inserted
replaced
520 qed |
520 qed |
521 |
521 |
522 |
522 |
523 subsection \<open>Cancellation simprocs\<close> |
523 subsection \<open>Cancellation simprocs\<close> |
524 |
524 |
|
525 lemma add_diff_cancel_enat[simp]: "x \<noteq> \<infinity> \<Longrightarrow> x + y - x = (y::enat)" |
|
526 by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl) |
|
527 |
525 lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c" |
528 lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c" |
526 unfolding plus_enat_def by (simp split: enat.split) |
529 unfolding plus_enat_def by (simp split: enat.split) |
527 |
530 |
528 lemma enat_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b \<le> c" |
531 lemma enat_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b \<le> c" |
529 unfolding plus_enat_def by (simp split: enat.split) |
532 unfolding plus_enat_def by (simp split: enat.split) |