∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hJ : hI.IsSubDPIdeal J)
  [inst_1 : (x : A) → Decidable (x ∈ J)] {n : ℕ} {a : A},
  a ∈ J → (DividedPowers.IsSubDPIdeal.dividedPowers hI hJ).dpow n a = hI.dpow n a