[bubblyworld]

Yeah, I think you have to exclude 0 to push that proof through. Your relation is still well-ordered in that case so it's fine I think.