Chinese Remainder Theorem
-------------------------

------
Summary:
Needs many lemmas (some of whose proofs are also challenging)
An Existential Witness has to be Provided
------

Definitions:

allcongruent
------------
(num, list) -> bool

allcongruent(x, nil) = true
allcongruent(x, y::z) = allcongruent(x, z) and (rem(x, first(y))=rem(second(y), first(y)))

allpositive
-----------
list -> bool

true if all members of the list are greater than 0.

allprime2
---------
list -> bool

allprime2(nil) = true
allprime2(y::z) = prime2list(x, first(y)) and allprime2(x, z)

prime2
------
is true iff its argumens are relatively prime

prime2list
----------
(num, list) -> bool

prime2list(x, nil) = true
prime2list(x, y::z) = prime2(x, first(y)) and prime2list(x, z)

products1
---------
product of list.

rem
---
returns the remainder of x by y


------
Theorem:
forall l:(list (pair nat)). exists x:nat. 
	(allpositive(l) and allprime2(l)) -> allcongruent(x,l)
forall l:(list (pair nat)). forall x,y:nat. 
	((allpositive(l) and allprime2(l)) and allcongruent(x,l)
	and allcongruent(y,l)) -> (mod (x - y),products(l)) 

Comments
--------
Actually two proof, existance and uniqueness.

Proved in RRL by Zhang and Hua and there is a good deal of comment of
the proof in their CADE-11 paper on the subject.

They provide by hand the existential witness needed for the existance
part of the proof.

Source
------
Proving the Chinese Remainder Theorem by the Cover Set Induction,
H. Zhang and X. Hua, CADE-11, D. Kapur (ed), 1992.  Springer-Verlag.