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_catin this case. This also allowed simplifying another proof in the file.
- Use automation more effectively.
- Use ssreflect's
addn1rather than the convoluted
replaced.... with ...; last by ...pattern.