∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : Preorder R] {a : R} [inst_2 : Preorder α] {f : α → R}
  [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R],
  Antitone f → a ≤ 0 → Monotone fun x => a * f x