| changeset 58770 | ae5e9b4f8daf |
| parent 58740 | cb9d84d3e7f2 |
| child 58874 | 7172c7ffb047 |
| 58769:70fff47875cd | 58770:ae5e9b4f8daf |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Useful Numerical Lemmas *} |
5 header {* Useful Numerical Lemmas *} |
6 |
6 |
7 theory Misc_Numeric |
7 theory Misc_Numeric |
8 imports Main Parity |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 lemma mod_2_neq_1_eq_eq_0: |
11 lemma mod_2_neq_1_eq_eq_0: |
12 fixes k :: int |
12 fixes k :: int |
13 shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0" |
13 shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0" |