equal
deleted
inserted
replaced
388 apply (blast dest: DERIV_unique order_less_imp_le) |
388 apply (blast dest: DERIV_unique order_less_imp_le) |
389 done |
389 done |
390 |
390 |
391 lemma mod_exhaust_less_4: |
391 lemma mod_exhaust_less_4: |
392 "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)" |
392 "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)" |
393 by (case_tac "m mod 4", auto, arith) |
393 by auto |
394 |
394 |
395 lemma Suc_Suc_mult_two_diff_two [rule_format, simp]: |
395 lemma Suc_Suc_mult_two_diff_two [rule_format, simp]: |
396 "0 < n --> Suc (Suc (2 * n - 2)) = 2*n" |
396 "0 < n --> Suc (Suc (2 * n - 2)) = 2*n" |
397 by (induct "n", auto) |
397 by (induct "n", auto) |
398 |
398 |