numbertheory Proof of coursework 1 for the Imperial number theory course The main result is the lemma question_4 in src/question.lean