## Addition is only declared as `Commutative` in iris

Just learned that addition on naturals is not "commutative" for stdpp, but only in Iris. Take the following proof:

```
Require Import iris.algebra.base iris.algebra.cmra.
Lemma foo i j: i + j = j + i. Proof. rewrite {1}[_ + _]comm //. Qed.
```

That works, but the instance found for `Commutative`

is `@cmra_comm natR`

.
But if we load the whole stdpp (and algebra.base to get ssreflect), no instance is found. After:

```
Require Import iris.algebra.base stdpp.prelude.
Lemma foo i j: i + j = j + i. Proof. Fail rewrite {1}[_ + _]comm //. Qed.
```

we get:

```
The command has indeed failed with message:
Ltac call to "rewrite (ssrrwargs) (ssrclauses)" failed.
pattern (i + j) does not match LHS of comm
```

I'm creating an issue because this instance might have been omitted on purpose, and code might be relying on its absence accidentally. But I expect this isn't for performance reasons — or the instance we currently get would already be a problem.

Instance `@cmra_assoc natR`

might cause similar concerns, but I haven't checked; other instances might as well, but it's less clear how.

I also wonder whether something more should be `Typeclasses Opaque`

(say, `nat_op`

?), to avoid this instance triggering accidentally, tho I'm not sure that's possible.