{u : Lean.Level} →
  {α : Q(Type u)} →
    (pα : Q(PartialOrder «$α»)) →
      (instα : Q(AddCommMonoid «$α»)) →
        (motive : Lean.LOption Q(IsOrderedCancelAddMonoid «$α») → Sort u_1) →
          (__discr : Lean.LOption Q(IsOrderedCancelAddMonoid «$α»)) →
            ((pα' : Q(IsOrderedCancelAddMonoid «$α»)) → motive (Lean.LOption.some pα')) →
              ((x : Lean.LOption Q(IsOrderedCancelAddMonoid «$α»)) → motive x) → motive __discr