diff -r b04508c59b9d -r 2488fc510178 src/HOL/NumberTheory/Int2.thy
--- a/src/HOL/NumberTheory/Int2.thy	Mon Dec 17 18:24:44 2007 +0100
+++ b/src/HOL/NumberTheory/Int2.thy	Mon Dec 17 18:27:48 2007 +0100
@@ -124,13 +124,7 @@
 
 lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
     x < m; y < m |] ==> x = y"
-  apply (simp add: zcong_zmod_eq)
-  apply (subgoal_tac "(x mod m) = x")
-  apply (subgoal_tac "(y mod m) = y")
-  apply simp
-  apply (rule_tac [1-2] mod_pos_pos_trivial)
-  apply auto
-  done
+  by (metis zcong_not zcong_sym zless_linear)
 
 lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
     ~([x = 1] (mod p))"