equal
deleted
inserted
replaced
486 lemma [presburger]: |
486 lemma [presburger]: |
487 "even n \<longleftrightarrow> even (int n)" |
487 "even n \<longleftrightarrow> even (int n)" |
488 by simp |
488 by simp |
489 |
489 |
490 |
490 |
491 subsection \<open>Nice facts about division by @{term 4}\<close> |
491 subsection \<open>Nice facts about division by \<^term>\<open>4\<close>\<close> |
492 |
492 |
493 lemma even_even_mod_4_iff: |
493 lemma even_even_mod_4_iff: |
494 "even (n::nat) \<longleftrightarrow> even (n mod 4)" |
494 "even (n::nat) \<longleftrightarrow> even (n mod 4)" |
495 by presburger |
495 by presburger |
496 |
496 |