∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : Preorder R] [inst_2 : Preorder α] {f g : α → R}
  [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R],
  Antitone f → Monotone g → (∀ (x : α), f x ≤ 0) → (∀ (x : α), 0 ≤ g x) → Antitone (f * g)