## shorten proof of task_arrivals_up_to_prefix_cat

Here's an example of how to simplify the proof that I pointed out today. I did three things:

- Pull out a useful intermediate lemma,
`task_arrivals_between_cat`

in this case. This also allowed simplifying another proof in the file. - Use automation more effectively.
- Use ssreflect's
`rewrite`

with`addn1`

rather than the convoluted`replaced.... with ...; last by ...`

pattern.