changeset 56537 | 01caba82e1d2 |
parent 56536 | aefb4a8da31f |
child 56889 | 48a745e1bde7 |
--- a/src/HOL/Library/Extended_Real.thy Fri Apr 11 13:36:57 2014 +0200 +++ b/src/HOL/Library/Extended_Real.thy Fri Apr 11 17:11:41 2014 +0200 @@ -536,7 +536,7 @@ lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))" unfolding incseq_def by auto -lemma ereal_add_nonneg_nonneg: +lemma ereal_add_nonneg_nonneg[simp]: fixes a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b" using add_mono[of 0 a 0 b] by simp