## Summary Port [`algebra/lib/ufrac_auth.v`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/lib/ufrac_auth.v). ## Subtasks - [ ] Lemmas - [ ] Updates - [ ] Functors ## Dependencies **Rocq dependencies:** - #261 - #240 - #229 - #241 - #231
Summary
Port
algebra/lib/ufrac_auth.v.Subtasks
Dependencies
Rocq dependencies: