∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} [inst_1 : SizeOf A] (carrier : Ideal A)
  (isSubideal : carrier ≤ I) (dpow_mem : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier, hI.dpow n j ∈ carrier),
  sizeOf { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem } = 1 + sizeOf carrier