Abstract
This work presents a formalisation of a generating function proof for
Lucas's theorem. We first outline extensions to the existing
Formal Power Series (FPS) library, including an equivalence relation
for coefficients modulo n, an alternate binomial theorem statement,
and a formalised proof of the Freshman's dream (mod p) lemma.
The second part of the work presents the formal proof of Lucas's
Theorem. Working backwards, the formalisation first proves a well
known corollary of the theorem which is easier to formalise, and then
applies induction to prove the original theorem statement. The proof
of the corollary aims to provide a good example of a formalised
generating function equivalence proof using the FPS library. The final
theorem statement is intended to be integrated into the formalised
proof of Hilbert's 10th Problem.