src/HOL/Hyperreal/HyperDef.thy

          del: star_of_zero)
 
 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
 by (simp add: epsilon_def omega_def star_n_inverse)
 
+lemma hypreal_epsilon_gt_zero: "0 < epsilon"
+by (simp add: hypreal_epsilon_inverse_omega)
+
 end