Adds the *discardable fractions camera*. This is a generalisation of the fractional camera where elements can represent both ownership of a fraction and the knowledge that a fraction has been discarded. One can make a frame preserving update from owning a fraction `q`

to knowing that `q`

has been discarded. The core is the identity function for the knowledge that `q`

has been discarded making ownership of such an element persistent.

Similarly to how with the authorative camera every element can be written as `● a ⋅ ◯ b`

and to how one use this to never write elements as pairs directly, every element of `dfrac`

can be written as `DfracOwn q ⋅ DfracDiscarded p`

and I imagine that one would use this to never use `DfracBoth`

. That's is why none of the lemmas mention `DfracBoth`

.