[STATEMENT]
lemma eint_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::eint) \<or> b \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a + b \<le> a + c) = (a = \<infinity> \<or> b \<le> c)
[PROOF STEP]
unfolding plus_eint_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((case a of eint m \<Rightarrow> case b of eint n \<Rightarrow> eint (m + n) | \<infinity> \<Rightarrow> \<infinity> | \<infinity> \<Rightarrow> \<infinity>) \<le> (case a of eint m \<Rightarrow> case c of eint n \<Rightarrow> eint (m + n) | \<infinity> \<Rightarrow> \<infinity> | \<infinity> \<Rightarrow> \<infinity>)) = (a = \<infinity> \<or> b \<le> c)
[PROOF STEP]
by (simp split: eint.split)