(a b : Q(ℤ)) →
  (motive : (r : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNat («$a» % -«$b») «$r») → Sort u_1) →
    (x : (r : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNat («$a» % -«$b») «$r»)) →
      ((r : Q(ℕ)) → (p : Q(Mathlib.Meta.NormNum.IsNat («$a» % -«$b») «$r»)) → motive ⟨r, p⟩) → motive x