equal
deleted
inserted
replaced
4 Copyright : 1999 University of Edinburgh |
4 Copyright : 1999 University of Edinburgh |
5 *) |
5 *) |
6 |
6 |
7 header{*Even and Odd Numbers: Compatibility file for Parity*} |
7 header{*Even and Odd Numbers: Compatibility file for Parity*} |
8 |
8 |
9 theory EvenOdd = NthRoot: |
9 theory EvenOdd |
|
10 import NthRoot |
|
11 begin |
10 |
12 |
11 subsection{*General Lemmas About Division*} |
13 subsection{*General Lemmas About Division*} |
12 |
14 |
13 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" |
15 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" |
14 apply (induct_tac "m") |
16 apply (induct_tac "m") |