feat: Deal with numbers

[markusdemedeiros]

Description

Fixes #267 plus bi/lib/mono_Z.v, and adds some extra stuff to IrisMath

This PR generally tidies up and completes the numbers CMRA's. It provides (scoped) instances for three classes of commutative monoids which cover every variant in Iris-Rocq. Cameras that use nonstandard Add instances are newtyped to avoid leaking the wrong instances.

I'll note that in doing this I found what I believe to be dead code in Iris-Rocq as well as missing instances. A win for generalization!

I like having a version that works for general commutative monoids because there are examples abound in mathlib, and I'd prefer to not copy-paste this for every numerical type. I presume that copy-paste was probably how Iris-Rocq ended up with dead instances.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

[markusdemedeiros]

(@lzy0505 You could also review this too if you have time)

[Kaptch]

Are these intended to be left here? Would you mind if I remove/move it to test file?

[markusdemedeiros]

Sure, go for it