{α : Type u_1} →
  [inst : Mul α] →
    [inst_1 : Zero α] →
      [inst_2 : Preorder α] →
        {motive : PosMulStrictMono α → Sort u} →
          ((mul_lt_mul_of_pos_left : ∀ ⦃a : α⦄, 0 < a → ∀ ⦃b c : α⦄, b < c → a * b < a * c) → motive ⋯) →
            (t : PosMulStrictMono α) → motive t