induction n generalizing f
f : ℝ → ℝ
a b : ℝ
hab : a < b
n : ℕ
h : ContDiffOn ℝ (↑n) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
case zero
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContDiffOn ℝ (↑Nat.zero) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑Nat.zero) g ∧ EqOn g f (Icc a b)

case succ
a b : ℝ
hab : a < b
n✝ : ℕ
n_ih✝ : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n✝) f (Icc a b) → ∃ g, ContDiff ℝ (↑n✝) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n✝)) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n✝)) g ∧ EqOn g f (Icc a b)