refactor(analysis/calculus/cont_diff): reorder the file (#13468)

* There are no functional changes in this PR (except the order of implicit arguments in some lemmas)
* This PR tries to move `cont_diff.comp` above some other lemmas. In a follow-up PR I will use this to add lemmas like `cont_diff.fst` which requires `cont_diff.comp`, but after this PR we can add it near `cont_diff_fst`.
* We also add `{m n : with_top ℕ}` as variables, so that we don't have to repeat this in every lemma