# HG changeset patch
# User paulson
# Date 976786211 -3600
# Node ID 3e4f5ae4faa6fdf107656c3a4b493b079a325ed4
# Parent  3b84288e60b718480a00fcacc643506cd2254b64
new theorem real_lbound_gt_zero

diff -r 3b84288e60b7 -r 3e4f5ae4faa6 src/HOL/Real/RealArith.ML
--- 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";