no goals
E : Type ?u.426364
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.426460
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
h_anti : AntitoneOn (deriv f) (interior D)
⊢ MonotoneOn (deriv (-f)) (interior D)
simpa only [← deriv.neg] using h_anti.neg