Irrationality of the square root of 2

[EgbertRijke]

The goal of this PR is twofold:

• To prove the irrationality of the square root of 2, and
• Cleaning up some of the elementary number theory files related to divisibility to make them more easily usable and understandable.

[fredrik-bakke]

Cool! I'll wait to submit the 100-theorems list to Freek until after this PR is merged :) #1203

[fredrik-bakke]

You're switching between using code guarded algebraic expressions in your headers and latex rendered ones in this PR. While code guarding is certainly the more established style in the library (there is only one place in the whole library where latex rendered text is used in a header:
https://unimath.github.io/agda-unimath/ring-theory.localizations-rings.html#the-type-of-localizations-of-a-ring-r-at-an-element-x-is-contractible), the LaTeX rendering looks a lot better in my opinion, so I'm tempted to suggest you use only latex rendered algebraic expressions in headers in your PR.