{α : Type u_2} →
  [inst : CommMonoid α] →
    [inst_1 : PartialOrder α] →
      {motive : IsOrderedCancelMonoid α → Sort u} →
        (t : IsOrderedCancelMonoid α) →
          ([toIsOrderedMonoid : IsOrderedMonoid α] →
              (le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c) →
                (le_of_mul_le_mul_right : ∀ (a b c : α), b * a ≤ c * a → b ≤ c) → motive ⋯) →
            motive t