Add discardable fractions camera

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.