diff -r fe6bcf0137b4 -r 7895c159d7b1 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jan 18 17:04:35 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jan 19 08:28:08 2018 +0100
@@ -923,6 +923,9 @@
 lemma e2ennreal_enn2ereal[simp]: "e2ennreal (enn2ereal x) = x"
   by (simp add: e2ennreal_def max_absorb2 ennreal.enn2ereal_inverse)
 
+lemma enn2ereal_e2ennreal: "x \<ge> 0 \<Longrightarrow> enn2ereal (e2ennreal x) = x"
+by (metis e2ennreal_enn2ereal ereal_ennreal_cases not_le)
+
 lemma e2ennreal_ereal [simp]: "e2ennreal (ereal x) = ennreal x"
 by (metis e2ennreal_def enn2ereal_inverse ennreal.rep_eq sup_ereal_def)