chore(number_theory/dioph): Cleanup (#13403)
Clean up, including:
* Move prerequisites to the correct files
* Make equalities in `poly` operations defeq
* Remove defeq abuse around `set`
* Slightly golf proofs by tweaking explicitness of lemma arguments
Renames
