equal
deleted
inserted
replaced
1202 apply (simp add: zmult_zless_cancel1) |
1202 apply (simp add: zmult_zless_cancel1) |
1203 apply (force dest: zless_add1_iff_zle [THEN iffD1] zless_trans zless_zle_trans) |
1203 apply (force dest: zless_add1_iff_zle [THEN iffD1] zless_trans zless_zle_trans) |
1204 apply (subgoal_tac "b$*q = r' $- r $+ b'$*q'") |
1204 apply (subgoal_tac "b$*q = r' $- r $+ b'$*q'") |
1205 prefer 2 apply (simp add: zcompare_rls) |
1205 prefer 2 apply (simp add: zcompare_rls) |
1206 apply (simp (no_asm_simp) add: zadd_zmult_distrib2) |
1206 apply (simp (no_asm_simp) add: zadd_zmult_distrib2) |
1207 apply (subst zadd_commute, rule zadd_zless_mono) |
1207 apply (subst zadd_commute [of "b $\<times> q'"], rule zadd_zless_mono) |
1208 prefer 2 apply (blast intro: zmult_zle_mono1) |
1208 prefer 2 apply (blast intro: zmult_zle_mono1) |
1209 apply (subgoal_tac "r' $+ #0 $< b $+ r") |
1209 apply (subgoal_tac "r' $+ #0 $< b $+ r") |
1210 apply (simp add: zcompare_rls) |
1210 apply (simp add: zcompare_rls) |
1211 apply (rule zadd_zless_mono) |
1211 apply (rule zadd_zless_mono) |
1212 apply auto |
1212 apply auto |