refactor(analysis/calculus/cont_diff): bit of cleanup (#17585)
* Move some lemmas further down in the file (so that we can use more properties about `cont_diff`)
* Rename `cont_diff_clm_apply` to `cont_diff_clm_apply_iff`
* From the sphere eversion project
* Part of #16946 (feel free to merge that PR directly instead of this one)
