Don't always "drill to the bottom" and unfold to sums; instead
explicitly make use of the fact that the EDF proof reasons about
finite identical prefixes, which allows staying at a semantically
higher level in the proof.

While at it, switch the file to using the preferred `now` tactical
when closing out proofs (rather than `by`) to avoid emacs indentation
issues.

Before mathcomp 1.11.0 (which requires Coq 8.12), case analysis
doesn't automatically rewrite destructed `minn` premises, so "try"
this manually until we drop support for mathcomp 1.11.0.

Can't rely on arg_maxnP just yet.

This change breaks compatibility with mathcomp < 1.10.

There's now also a `findP` in ssreflect's seq library.

add lemmas on consistency of backlogged jobs set

add notion of a non-clairvoyant readiness model

This is a general definition and not specific to a particular
implementation.

...by adding the -projection-no-head-constant flag to the build settings.

Vedant Chavda authored 4 years ago and Björn Brandenburg committed 4 years ago

change it to perm_big