mathlib3

a07d03ac - chore(analysis/calculus/cont_diff): Add two missing cont_diff_on lemmas (#16108)

chore(analysis/calculus/cont_diff): Add two missing cont_diff_on lemmas (#16108) Adds two lemmas that are immediate consequences of `cont_diff_on.of_le`. Names and proofs are taken verbatim from the corresponding `cont_diff` lemmas.