Port bi/algebra.v

## Summary

Port [`bi/algebra.v`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/bi/algebra.v).



## Dependencies








**Rocq dependencies:**

- #226
- #261
- #220
- #228
- #254
- #262
- #221
- #256
- #217
- #286