∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Preorder β] (f : α → β) (h_mono : StrictMono f)
  (g : β → α) (hg : Function.RightInverse g f), ⇑(StrictMono.orderIsoOfRightInverse f h_mono g hg) = f