This paper (ps, pdf), which was presented at ACL2 Workshop 2000 (see slides: ps, pdf), describes an ACL2 proof of the Chinese Remainder Theorem:
If m1, ..., mk are pairwise relatively prime moduli and a1, ..., ak are natural numbers, then there exists a natural number x that simultaneously satisfies x = ai (mod mi), i=1, ..., k.
The entire proof is
contained in the single event file
crt.lisp, except that it
depends on some lemmas from the author's
library of floating-point arithmetic.
In order to certify this file (after obtaining and certifying the library), first replace each
of the two occurrences of "
/u/druss/" with the path to the directory under which
your copy of the library resides. A second event file,
which contains the definitions and main lemmas involved in the proof, may then be certified.