PDF cleanup 282: rename sucᵉ to 1 +ᵉ_

[williamdemeo]

Description

Second attempt to rename sucᵉ, this time using a simpler approach---simply replace it with 1 +ᵉ_.

This addresses one item of issue #282.

Maybe this is not idea, but I'm not sure there's a better alternative if we can't identify Epoch as one of the simple/standard types of algebraic structures for which there is already support for literals.

It was suggested in the comments of previous PR #315 (since closed) that Epoch has a module structure, but I don't see it. To me Epoch looks more like a G-set, where the group acting on Epoch is ℕ` ...and I don't know if there's support for G-set literals ...yet. If there is
not, then we could develop it, but I'm not sure it's worth doing for the sole purpose of renaming one symbol.

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

[WhatisRT]

It'd be better to instead make an epoch 1ᵉ, so that you can write 1ᵉ +_ for sucᵉ. That way we can then just use literal overloading to get rid of the ᵉ entirely.

[williamdemeo]

It'd be better to instead make an epoch 1ᵉ, so that you can write 1ᵉ +_ for sucᵉ. That way we can then just use literal overloading to get rid of the ᵉ entirely.

Okay, I'll try that... I'm not sure off the top of my head how 1ᵉ should be defined off the top of my head, but I'll look again at the code and see if I can figure it out... If not, I'll ask.

[WhatisRT]

Closing in favour of #387