∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β]
  {s : Set β} {a : α}, a < 0 → BddAbove (a • s) = BddBelow s