equal
deleted
inserted
replaced
299 apply (rule zless_imp_add1_zle) |
299 apply (rule zless_imp_add1_zle) |
300 apply (erule (1) mult_right_less_imp_less) |
300 apply (erule (1) mult_right_less_imp_less) |
301 apply assumption |
301 apply assumption |
302 done |
302 done |
303 |
303 |
304 lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified] |
304 lemmas less_le_mult = less_le_mult' [simplified distrib_right, simplified] |
305 |
305 |
306 lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, |
306 lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, |
307 simplified left_diff_distrib] |
307 simplified left_diff_distrib] |
308 |
308 |
309 lemma lrlem': |
309 lemma lrlem': |