Clean up bf_update_range_ok proof
Clean up bf_update_range_ok proof

- Fixed the admits to reflect what is actually left. There's some proof
  duplication between two goals step generates, not sure how to avoid
  that.
- Made better use of eapply/eauto. In the case of bfrec_bound,
  eassumption in order on the hypotheses caused some incorrect
  instantiations, so I fixed the order of hypotheses (hopefully that
  didn't break another proof).
- The proof itself is now shorter and better organized. Made use of now
  to help make clear when things are being finished. There may still be
  some higher-level lemmas to collapse parts of this proof.

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl