{u : Lean.Level} →
  {α : Q(Type u)} →
    {a : Q(«$α»)} →
      (_ir : Q(Ring «$α»)) →
        (motive : ℤ × (lit : Q(ℤ)) × Q(Mathlib.Meta.NormNum.IsInt «$a» «$lit») → Sort u_1) →
          (__discr : ℤ × (lit : Q(ℤ)) × Q(Mathlib.Meta.NormNum.IsInt «$a» «$lit»)) →
            ((za : ℤ) → (na : Q(ℤ)) → (pa : Q(Mathlib.Meta.NormNum.IsInt «$a» «$na»)) → motive (za, ⟨na, pa⟩)) →
              motive __discr