new theorem real_lbound_gt_zero

--- a/src/HOL/Real/RealArith.ML	Wed Dec 13 17:46:49 2000 +0100
+++ b/src/HOL/Real/RealArith.ML	Thu Dec 14 10:30:11 2000 +0100
@@ -383,3 +383,7 @@
                                       real_inverse_less_iff]) 1); 
 qed "real_inverse_le_iff";
 
+Goal "[| (#0::real) < d1; #0 < d2 |] ==> EX e. #0 < e & e < d1 & e < d2";
+by (res_inst_tac [("x","(min d1 d2)/#2")] exI 1); 
+by (asm_simp_tac (simpset() addsimps [min_def]) 1); 
+qed "real_lbound_gt_zero";