∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableLT α] (a b : α),
  a ≤ b →
    (fun a => if 0 < a then 1 else if a < 0 then -1 else 0) a ≤
      (fun a => if 0 < a then 1 else if a < 0 then -1 else 0) b