## Discardable camera improvements

## Generalization

I think the variant of `dfrac`

that I implemented with !531 (merged) can be generalized to a "discardable-anything":

```
Inductive discardable (A: cmraT) :=
| DOwn : A → dfrac
| DDiscarded : dfrac
| DBoth : A → dfrac.
```

with validity something like

```
Instance discardable_valid (A: cmraT) : Valid (discardable A) := λ x,
match x with
| DOwn q => ✓ q
| DDiscarded => True
| DBoth q => exists p, ✓ (q ⋅ p)
end%Qc.
```

I think this should work... what I am not sure about is if this is useful.^^

##
discarded idea: `option Qp`

old After !531 (merged), the public interface of `dfrac`

can basically be described via a smart constructor that takes `option Qp`

-- in fact I am adding such a notation in !486 (merged). We can probably rephrase all the existing lemmas in terms of that single constructor, and @robbertkrebbers agrees that that would make a better interface.