changeset 10669 | 3e4f5ae4faa6 |
parent 10660 | a196b944569b |
child 10677 | 36625483213f |
--- 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";