--- a/Quot/Examples/IntEx2.thy	Wed Dec 09 22:05:11 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Wed Dec 09 22:43:11 2009 +0100
@@ -202,11 +202,19 @@
 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 add:
      "(ABS_int (x,y)) + (ABS_int (u,v)) =
       (ABS_int (x+u, y+v))"
 apply(simp add: plus_int_def)
-sorry
+apply(fold plus_raw.simps)
+apply(rule Quotient_rel_abs[OF Quotient_int])
+apply(rule plus_raw_rsp_lo)
+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)