Saying something without saying anything in #lean:

def non_decreasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : non_decreasing (g ∘ f) := fun _ _ h => hg _ _ (hf _ _ h)

Is this a good proof? It's certainly easy to see after seeing it !!