(* ------------------------------------------------------------------------- *)
(* Hierarchy of Tools Library                                                *)
(*                                                                           *)
(* Author: Joseph Chan                                                       *)
(* Date: December, 2014                                                      *)
(* ------------------------------------------------------------------------- *)

0 helperNum -- extends HOL library on numbers.
* divides
* gcd

1 helperSet -- extends HOL library on sets.
* pred_set
* 0 helperNum

1 helperList -- extends HOL library on lists.
* pred_set
* list
* rich_list
* listRange
* 0 helperNum

2 helperFunction -- useful theorems on functions.
* 0 helperNum
* 1 helperList
* 1 helperSet

2 sublist -- order-preserving sublist and properties.
* 0 listRange
* 1 helperList

3 logPower -- properties of perfect power, power free, and upper logarithm.
* logroot
* 0 helperNum
* 0 helperSet
* 2 helperFunction

3 binomial -- properties of binomial coefficients in Pascal's Triangle.
* 0 helperNum
* 1 helperSet
* 1 helperList
* 2 helperFunction

3 Euler -- number-theoretic sets, and Euler's phi function.
* 0 helperNum
* 1 helperSet
* 2 helperFunction

4 Gauss -- coprimes, properties of phi function, and Gauss' Little Theorem.
* 0 helperNum
* 1 helperSet
* 1 helperList
* 2 helperFunction
* 3 Euler

4 primes -- properties of two-factors, and a primality test.
* 0 helperNum
* 2 helperFunction
* 3 logPower

4 triangle -- properties of Leibniz's Denominator Triangle, relating to consecutive LCM.
* listRange
* relation
* 0 helperNum
* 1 helperSet
* 1 helperList
* 2 helperFunction
* 3 binomial
* 3 Euler

5 primePower -- properties of prime powers and divisors, an investigation on consecutive LCM.
* listRange
* option
* 0 helperNum
* 1 helperSet
* 1 helperList
* 2 helperFunction
* 3 logPower
* 3 Euler
* 4 triangle

5 Mobius -- work on Mobius Inversion.
* 0 helperNum
* 1 helperSet
* 1 helperList
* 3 Euler
* 4 Gauss