Post #1458441

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 !!