(a m b hi c1 : Q(ℕ)) →
  (motive :
      (c : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNatPowModT ((«$a».pow «$hi»).mod «$m» = «$c1») «$a» «$b» «$m» «$c») →
        Sort u_1) →
    (x : (c : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNatPowModT ((«$a».pow «$hi»).mod «$m» = «$c1») «$a» «$b» «$m» «$c»)) →
      ((c2 : Q(ℕ)) →
          (p2 : Q(Mathlib.Meta.NormNum.IsNatPowModT ((«$a».pow «$hi»).mod «$m» = «$c1») «$a» «$b» «$m» «$c2»)) →
            motive ⟨c2, p2⟩) →
        motive x