Greatly simplify chunkList proofs
Greatly simplify chunkList proofs

- used Program Fixpoint to define the isplit_dep obligations as well
  (removing the helper lemmas).
- introduced min_cases lemma which splits min n m into either n < m and
  min n m = n, or n >= m and min n m = m. Omega can then usually just
  solve the system, now that min is replaced with an equality and an
  expression. This makes all the obligations straightforward, with the
  remaining proof handled by the fact that a mod m < m (only used for
  m = blocksize, but true whenever m > 0).

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