# HG changeset patch
# User paulson
# Date 952528399 -3600
# Node ID 0fda5ba36934de3fedd828764781e8f5330af704
# Parent  1b8ac0f482336c08c7a0d19bdeffcff5abacbece
new lemmas

diff -r 1b8ac0f48233 -r 0fda5ba36934 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Mon Mar 06 21:10:27 2000 +0100
+++ b/src/HOL/Arith.ML	Wed Mar 08 16:13:19 2000 +0100
@@ -610,8 +610,7 @@
 qed "Suc_mult_cancel1";
 
 
-(** Lemma for gcd **)
-
+(*Lemma for gcd*)
 Goal "m = m*n ==> n=1 | m=0";
 by (dtac sym 1);
 by (rtac disjCI 1);
@@ -1158,3 +1157,20 @@
 Goal "[| m-n = 0; n-m = 0 |] ==>  m=n";
 by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
 qed "diffs0_imp_equal";
+
+(** Lemmas for ex/Factorization **)
+
+Goal "[| 1<n; 1<m |] ==> 1<m*n";
+by (exhaust_tac "m" 1);
+by Auto_tac;
+qed "one_less_mult"; 
+
+Goal "[| 1<n; 1<m |] ==> n<m*n";
+by (exhaust_tac "m" 1);
+by Auto_tac;
+qed "n_less_m_mult_n"; 
+
+Goal "[| 1<n; 1<m |] ==> n<n*m";
+by (exhaust_tac "m" 1);
+by Auto_tac;
+qed "n_less_n_mult_m";