# HG changeset patch
# User wenzelm
# Date 880559154 -3600
# Node ID 5defc2105cc890d18eb1bb8230f4a76bf8defb8e
# Parent  aa84d9c6245470fdb6eddd727adaa72e6f114184
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;

diff -r aa84d9c62454 -r 5defc2105cc8 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Nov 26 16:44:47 1997 +0100
+++ b/src/HOL/Arith.ML	Wed Nov 26 16:45:54 1997 +0100
@@ -557,6 +557,16 @@
 qed "mult_less_cancel1";
 Addsimps [mult_less_cancel1, mult_less_cancel2];
 
+goal Arith.thy "(Suc k * m < Suc k * n) = (m < n)";
+br mult_less_cancel1 1;
+by (Simp_tac 1);
+qed "Suc_mult_less_cancel1";
+
+goalw Arith.thy [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
+by (simp_tac (simpset_of HOL.thy) 1);
+br Suc_mult_less_cancel1 1;
+qed "Suc_mult_le_cancel1";
+
 goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
 by (cut_facts_tac [less_linear] 1);
 by Safe_tac;
@@ -571,6 +581,11 @@
 qed "mult_cancel1";
 Addsimps [mult_cancel1, mult_cancel2];
 
+goal Arith.thy "(Suc k * m = Suc k * n) = (m = n)";
+br mult_cancel1 1;
+by (Simp_tac 1);
+qed "Suc_mult_cancel1";
+
 
 (** Lemma for gcd **)