∀ {α : Type u} {β : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] (f : β → α),
  (∀ (x y : β), f (x + y) = f x + f y) → (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) → IsOrderedCancelAddMonoid β