Lifting the Exponent

We formalize the Lifting the Exponent Lemma, which shows how to find the largest power of $p$ dividing $a^n \pm b^n$, for a prime $p$ and positive integers $a$ and $b$. The proof follows Amir Hossein Parvardi's.