∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → ∀ {o : Ordering}, o.Compares (f a) (f b) ↔ o.Compares a b