equal
deleted
inserted
replaced
262 |
262 |
263 lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0" |
263 lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0" |
264 by (cut_tac n = 0 in mod2_add_more, auto) |
264 by (cut_tac n = 0 in mod2_add_more, auto) |
265 |
265 |
266 |
266 |
267 subsection\<open>Additional theorems about @{text "\<le>"}\<close> |
267 subsection\<open>Additional theorems about \<open>\<le>\<close>\<close> |
268 |
268 |
269 lemma add_le_self: "m:nat ==> m \<le> (m #+ n)" |
269 lemma add_le_self: "m:nat ==> m \<le> (m #+ n)" |
270 apply (simp (no_asm_simp)) |
270 apply (simp (no_asm_simp)) |
271 done |
271 done |
272 |
272 |