{u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      (pα : Q(PartialOrder «$α»)) →
        (a : Q(«$α»)) →
          (motive : Mathlib.Meta.Positivity.Strictness zα pα a → Sort u_1) →
            (ra : Mathlib.Meta.Positivity.Strictness zα pα a) →
              ((pa : Q(0 < «$a»)) → motive (Mathlib.Meta.Positivity.Strictness.positive pa)) →
                ((pa : Q(0 ≤ «$a»)) → motive (Mathlib.Meta.Positivity.Strictness.nonnegative pa)) →
                  ((pa : Q(«$a» ≠ 0)) → motive (Mathlib.Meta.Positivity.Strictness.nonzero pa)) →
                    (Unit → motive Mathlib.Meta.Positivity.Strictness.none) → motive ra