use mult_strict_mono instead of real_mult_less_mono

--- a/src/HOL/Hyperreal/Transcendental.thy	Fri May 18 11:12:03 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri May 18 16:11:13 2007 +0200
@@ -1261,8 +1261,8 @@
 apply (subst fact_lemma) 
 apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
 apply (simp only: real_of_nat_mult)
-apply (rule real_mult_less_mono, force)
-  apply (rule_tac [3] real_of_nat_fact_gt_zero)
+apply (rule mult_strict_mono, force)
+  apply (rule_tac [3] real_of_nat_fact_ge_zero)
  prefer 2 apply force
 apply (rule real_of_nat_less_iff [THEN iffD2])
 apply (rule fact_less_mono, auto)