chore(analysis/calculus/cont_diff): Add two helper lemmas (#15894)
chore(analysis/calculus/cont_diff): Add two helper lemmas (#15894)

This PR adds the forward direction of `cont_diff_iff_continuous_differentiable` as separate lemmas, which enables using dot-notation for `cont_diff`.





leanprover-community/mathlib,leanprover-community/mathlib