simplify structure of behavior, move arrival_sequence and schedule to toplevel, move task and sequential to model

- Consistently use JobType rather than eqType directly.
- Fix the comments style.

Coqdoc produces really nice output - let's automate this.

There's no need to run this for every compiler version; we only care
about the "main" version.

This avoids having to compile ssreflect from scratch each time we want
to compile Prosa.

Thanks to Pierre Roux (Pierre.Roux@onera.fr) for pointing out the
mathcomp Docker images!

From the mathcomp 1.9.0 release notes:

> removed Coq prelude hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm, to
> improve robustness of by ...; scripts may need to invoke addn0,
> addnS, muln0 or mulnS explicitly where these hints were used
> accidentally.

=> This patch makes these required fixes in Prosa.

While at it, turn on CI for coq:dev and Coq 8.9 with two versions of ssreflect.

Using the official Coq Docker images kindly provided by the Coq community:

	https://github.com/coq-community/docker-coq/wiki/CI-setup

Using the following CI template as a starting point:

	https://gitlab.com/erikmd/docker-coq-gitlab-ci-demo-1/blob/master/.gitlab-ci.yml

...and introduce a bunch of helper lemmas to get there.

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