Banker's Queue, verified
Remaining cleanup TODOs:
- in Streams.v, some lemmas about the previous definition of subdebits are commented out. They should be either deleted or revived (but they were not used in any case)
- some tactic helpers are duplicated between Streams.v and bqueue/Proof.v, they need to be factored out in some way or another.