{u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      (pα : Q(PartialOrder «$α»)) →
        {e : Q(«$α»)} →
          (motive : Mathlib.Meta.Positivity.Strictness zα pα e → Sort u_1) →
            (x : Mathlib.Meta.Positivity.Strictness zα pα e) →
              ((pf : Q(0 < «$e»)) → motive (Mathlib.Meta.Positivity.Strictness.positive pf)) →
                ((pf : Q(«$e» ≠ 0)) → motive (Mathlib.Meta.Positivity.Strictness.nonzero pf)) →
                  ((x : Mathlib.Meta.Positivity.Strictness zα pα e) → motive x) → motive x