Implement monotone partial bijections as a view
This is an alternative to !91 (closed), which was written prior to views. Using the view CMRA we factor the implementation into purely algebraic library and a logic-level wrapper. The logic-level wrapper exports resources which seal away the underlying ownership and has theorems which handle the ownership reasoning.
One thing I tried to do here is write the motivation for the library, as a comment in the logic-level own_bij.v library. I didn't understand the point of the library until @jung explained it to me.