
1 IntPrimes dvd relation, GCD, Euclid's extended algorithm, primes, 

2 congruences (all on the Integers) 

3 Comparable to 'Primes' theory but dvd is included here 

4 as it is not present in 'IntDiv'. Also includes extended 

5 GCD and congruences not present in 'Primes'. 

6 Also a few extra theorems concerning 'mod' 

7 Maybe it should be split/merged  at least given another 

8 name? 

9 

10 Chinese The Chinese Remainder Theorem for an arbitrary finite 

11 number of equations. (The oneequation case is included 

12 in 'IntPrimes') 

13 Uses functions for indicing. Maybe 'funprod' and 'funsum' 

14 should be based on general 'fold' on indices? 

15 

16 IntPowerFact Power function on Integers (exponent is still Nat), 

17 Factorial on integers and recursively defined set 

18 including all Integers from 2 up to a. Plus definition 

19 of product of finite set. 

20 Should probably be split/merged with other theories? 

21 

22 BijectionRel Inductive definitions of bijections between two different 

23 sets and between the same set. Theorem for relating 

24 the two definitions 

25 

26 EulerFermat Fermat's Little Theorem extended to Euler's Totient function. 

27 More abstract approach than BoyerMoore (which seems necessary 

28 to achieve the extended version) 

29 

30 WilsonRuss Wilson's Theorem following quite closely Russinoff's approach 

31 using BoyerMoore (using finite sets instead of lists, though) 

32 

33 WilsonBij Wilson's Theorem using a more "abstract" approach based on 

34 bijections between sets. Does not use Fermat's Little Theorem 

35 (unlike Russinoff) 

36 

37 