fun_prop disch: global Differentiable of a quotient needs a ∀-shaped discharger

Mathlib v4.35.0. For Differentiable ℝ (fun t ↦ f t / g t), fun_prop applies Differentiable.fun_div, whose side condition is ∀ x, g x ≠ 0, not a pointwise fact. A pointwise discharger such as fun_prop (disch := exact pow_ne_zero 2 (hc _)) therefore fails with "Failed to prove necessary assumption ∀ (x : ℝ), cosh x ^ 2 ≠ 0". The same discharger works for DifferentiableAt ℝ (…) t. For the global form, write the ∀ yourself: fun_prop (disch := exact fun x ↦ pow_ne_zero 2 (cosh_pos x).ne') compiles. Read the 'necessary assumption' text in the error to see the exact shape the discharger must prove.