Delete and add theorems in set-mbox-ii.

[expln]

cu3addi and cu3add have been deleted because they can be easily derived from cu3addd when needed.

Three new theorems have been added - sqnegd, anpnaneq0d, and rexlimdvv3d. They will be used in the proof of 3cubes (which I will add in one of my next pull requests).

Please help me to come up with a good name for anpnaneq0d (if its current name is not good enough). Currently it stands for “A to the power of N plus negative A to the power of N equals 0”.

Update:
anpnaneq0d is renamed to negexpidd.

[icecream17]

I think it's fine, but maybe negexpid (a la https://us.metamath.org/mpeuni/negid.html ) if necessary

And this gives me some ideas to shorten oexpreposd, awesome

[expln]

I think it's fine, but maybe negexpid (a la https://us.metamath.org/mpeuni/negid.html ) if necessary

And this gives me some ideas to shorten oexpreposd, awesome

negexpid is easier to remember, so I renamed. Thanks.