If `f x ≤ f y → x ≤ y`, then `f` is injective

Stream: Is there code for X?

[Anne Baanen]

I can't quite find the following result in the library:

lemma injective_of_le_imp_le {α β : Type*} [partial_order α] [preorder β] (f : α → β)
  (h : ∀ {x y}, f x ≤ f y → x ≤ y) : function.injective f :=
λ x y hxy, le_antisymm (h hxy.le) (h hxy.ge)

(In fact, I have docs#strict_mono since f x ≤ f y ↔ x ≤ y, but docs#strict_mono.injective requires a linear_order assumption.)

[Anne Baanen]

The closest I could find was docs#injective_of_lt_imp_ne, but that again requires linear_order.

[Anne Baanen]

Since there isn't any response: #8373