∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : SizeOf R]
  [inst_4 : SizeOf M] (toAddSubmonoid : AddSubmonoid M)
  (smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier),
  sizeOf { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' } = 1 + sizeOf toAddSubmonoid