Let's not clutter up the spec with facts files all over the place.
Instead, let's collect the facts files in a separate folder /
hierarchy.

- port completed_implies_scheduled_before
- port lemmas on service prior to arrival
- port scheduled_implies_pending and greatly simplify the proof while at it
- port and simplify job_pending_at_arrival
- port cumulative_service_implies_scheduled and simplify proof of
  positive_service_implies_scheduled_before
- port service_is_a_step_function

...from model/schedule/uni/schedule.v.

To simplify some of the rather long proofs in the original file, the patch introduces a bunch of small and simple rewriting and helper lemmas that we previously lacked, but that we *should* have to avoid having to reason at the level of sslreflect "big" operators in every lemma.

If one names a branch "something-something-file.v", then the current
script will find it in the .git directory and try to compile git's
branch description as a Coq file...

See https://beyondgrep.com/ for details.

Initial draft of the base for the behavior part of the refactored hierarchy. Implements most of the proposal discussed in Braunschweig.

The proof got stuck at the goal of

	 {in l1, forall x0 : T, x0 != x}

which requires unfolding of prop_in1 to get at the x0 before intros
can be effective.

1) Formalize the notion of weakly sustainable policy, along with
its contrapositive, and prove the equivalence between the two.

2) Establish weak sustainability of self-suspending tasks w.r.t.
execution times and variable suspension times, based on the
transformation we had formalized.