From the block inequality to the packing bound

• AaronsonAmbainis.packingBound_of_block : BlockInequality → PackingBound (Lemma 6.5 of the paper from Lemma 6.4; the proof is in Pack/Packing.lean)