mathlib

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

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