src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Sun Feb 24 20:18:32 2013 +0100
+++ b/src/HOL/Nat.thy	Sun Feb 24 20:29:13 2013 +0100
@@ -1201,6 +1201,16 @@
     apply (auto)
   done
 
+lemma mono_times_nat:
+  fixes n :: nat
+  assumes "n > 0"
+  shows "mono (times n)"
+proof
+  fix m q :: nat
+  assume "m \<le> q"
+  with assms show "n * m \<le> n * q" by simp
+qed
+
 text {* the lattice order on @{typ nat} *}
 
 instantiation nat :: distrib_lattice