feat(analysis/calculus/cont_diff): strengthen lemma (#16933)
* The new `cont_diff_within_at_succ_iff_has_fderiv_within_at'` generalizes `cont_diff_within_at.has_fderiv_within_at_nhds` and `cont_diff_within_at_succ_iff_has_fderiv_within_at_of_mem`
* Prove that `has_fderiv_within_at` and `cont_diff_within_at` are not dependent on adding a single point to the set
* Add some more lemmas needed for a follow-up PR
* From the sphere eversion project
