∀ {𝕜 : Type u_1} (G : Type u_2) [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup G] [inst_4 : PartialOrder G] [inst_5 : IsOrderedAddMonoid G] [inst_6 : Module 𝕜 G] {a : 𝕜}
  [inst_7 : PosSMulMono 𝕜 G] (ha : a < 0) (a_1 : G), (OrderIso.smulRightDual G ha) a_1 = a • OrderDual.toDual a_1