∀ {e' r : ℤ} {α : Type u_1} [inst : Ring α] {n n' : ℕ},
  CharP α n →
    ∀ {e : α},
      Mathlib.Meta.NormNum.IsInt e e' →
        Mathlib.Meta.NormNum.IsNat n n' → Mathlib.Meta.NormNum.IsInt (e' % ↑n') r → Mathlib.Meta.NormNum.IsInt e r