monotonicity lemma

Stream: general

[Rob Lewis]

I feel like this lemma (or similar) must exist somewhere already, but I'm coming up empty -- anyone recognize this?

example {α} [partial_order α] (f : ℕ → α) (h : ∀ n, f (n+1) ≤ f n) : ∀ m n, m ≤ n → f n ≤ f m