--- a/Quot/Examples/IntEx2.thy	Wed Dec 09 22:43:11 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Wed Dec 09 23:32:16 2009 +0100
@@ -180,7 +180,7 @@
 proof
   fix i j k :: int
   show "(i + j) + k = i + (j + k)"
-     by (lifting plus_assoc_raw)
+    by (lifting plus_assoc_raw)
   show "i + j = j + i" 
     by (lifting plus_sym_raw)
   show "0 + i = (i::int)"
@@ -201,26 +201,26 @@
     by (lifting one_zero_distinct)
 qed
 
-
-lemma plus_raw_rsp_lo:
-  "\<And>a b c d. a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> plus_raw a c \<approx> plus_raw b d"
-by auto
+lemma plus_raw_rsp_aux:
+  assumes a: "a \<approx> b" "c \<approx> d"
+  shows "plus_raw a c \<approx> plus_raw b d"
+using a
+by (cases a, cases b, cases c, cases d) 
+   (simp)
 
 lemma add:
      "(ABS_int (x,y)) + (ABS_int (u,v)) =
-      (ABS_int (x+u, y+v))"
+      (ABS_int (x + u, y + v))"
 apply(simp add: plus_int_def)
 apply(fold plus_raw.simps)
 apply(rule Quotient_rel_abs[OF Quotient_int])
-apply(rule plus_raw_rsp_lo)
+apply(rule plus_raw_rsp_aux)
 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
 done
 
-lemma int_def: "of_nat m = ABS_int (m, 0)"
-apply(induct m)
-apply(simp add: zero_int_def)
-apply(simp add: one_int_def add)
-done
+lemma int_def: 
+  shows "of_nat m = ABS_int (m, 0)"
+by (induct m) (simp_all add: zero_int_def one_int_def add)
 
 lemma le_antisym_raw:
   shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j"
@@ -284,26 +284,36 @@
 abbreviation
   "less_raw i j \<equiv> less_eq_raw i j \<and> \<not>(i \<approx> j)"
 
+lemma zmult_zless_mono2_lemma:
+  fixes i j::int
+  and   k::nat
+  shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
+apply(induct "k")
+apply(simp)
+apply(case_tac "k = 0")
+apply(simp_all add: left_distrib add_strict_mono)
+done
 
-lemma test:
-  "\<lbrakk>less_raw i j; less_raw (0, 0) k\<rbrakk>
-    \<Longrightarrow> less_raw (times_raw k i) (times_raw k j)"
-apply(cases i, cases j, cases k)
-apply(simp only: less_eq_raw.simps times_raw.simps)
-apply(simp)
-apply(rename_tac u v w x y z)
-apply(rule conjI)
-apply(subgoal_tac "y*u + y*x \<le> y*w + y*v  &  z*v \<le> y*v")
-apply(simp add: )
+lemma zero_le_imp_eq_int: 
+  fixes k::int
+  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
 sorry
 
+lemma zmult_zless_mono2: 
+  fixes i j k::int
+  assumes a: "i < j" "0 < k"
+  shows "k * i < k * j"
+using a
+apply(drule_tac zero_le_imp_eq_int)
+apply(auto simp add: zmult_zless_mono2_lemma)
+done
 
 text{*The integers form an ordered integral domain*}
 instance int :: ordered_idom
 proof
   fix i j k :: int
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
-    unfolding less_int_def by (lifting test)
+    by (rule zmult_zless_mono2)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
     by (simp only: abs_int_def)
   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"