equal
deleted
inserted
replaced
152 lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))" by arith |
152 lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))" by arith |
153 |
153 |
154 lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))" by arith |
154 lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))" by arith |
155 |
155 |
156 lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1] |
156 lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1] |
157 lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified] |
|
158 lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified] |
|
159 |
157 |
160 lemma z1pdiv2: |
158 lemma z1pdiv2: |
161 "(2 * b + 1) div 2 = (b::int)" by arith |
159 "(2 * b + 1) div 2 = (b::int)" by arith |
162 |
160 |
163 lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2, |
161 lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2, |