Refactor elementary number theory

[EgbertRijke]

The biggest changes come from a change in the definition of the quotient of a divisible natural number. The updated definition defines the quotient of n by d, provided that d | n is the unique natural number q ≤ n such that q * d = n. This change prevents some case analyses around the situation where the Curry-Howard interpretation of divisibility is not a proposition. An alternative definition of divisibility is also given: bounded divisibility. This is always a proposition. The poset of the natural numbers by divisibility is updated to use bounded divisibility in favor of propositional truncation.

The change in the definition of the quotient by divisibility triggered changes in the fundamental theorem of arithmetic, which is thoroughly revised after discovering that the strong induction that we previously used was unnecessarily complicated.

New files include:

• Bounded divisibility
• Irrationality of the square root of 2
• Lists of prime numbers
• Multiplicative decompositions of natural numbers
• Nicomachus's Theorem
• Nontrivial divisors of natural numbers
• Number of divisors
• Parity of integers
• Pronic numbers
• Square pyramidal numbers
• Unit integers
• Unit similarity integers
• Well-ordering principles of the integers
• Dependent lists
• Elementhood relation on lists
• Universal quantification on lists

[fredrik-bakke]

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