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.

1) Definition of a generic model for job suspensions based on
   received service (e.g., job j_1 should suspend for 4ms as
   soon as service reaches 5ms).

2) Definition of the dynamic suspension model (i.e., cumulative
   suspension of job j_1 <= X).

3) Analysis of suspension-aware scheduling by inflation of job
   costs (via schedule reduction). In the literature, this is
   called suspension-oblivious analysis.

4) Analysis of suspension-aware scheduling by adjusting job
   jitter (via schedule reduction).

5) Proof of (weak) sustainability of job costs under suspension-aware
   scheduling. We show that if we increase the costs of all jobs while
   reducing their suspension times in a certain way, the response times
   of all jobs do not decrease.

   This has an important implication regarding worst-case schedules: if
   some schedulability analysis already accounts for the fact that job
   suspension times can vary from 0 to the task suspension bound, then
   it's perfectly safe to assume that jobs execute for their WCET.

6) Proof of sustainability of the cost of a single job under
   suspension-aware scheduling. That is, we show that increasing the
   cost of a single job does not reduce its own response time.
   (Note that this is a very basic result that applies to many
   work-conserving, JLFP schedulers. We don't claim anything about
   the response time of other jobs.)

- Remove Require declarations from Modules.
- Small fixes due to changes in the type checker.
- Generate _CoqProject with Makefile and remove spurious warnings from ssreflect.

- Added definitions and implementation of jitter-aware RTA for
  uniprocessor scheduling.
- The Prosa directory was restructured to better accomodate the different
  types of arrival sequences and schedules.

- Add generic definition of job suspension based on the cumulative service
- Define the dynamic suspension model (based on task suspension bounds)
- Add suspension semantics for uniprocessor schedules
- Formalize reduction from suspension-aware schedule to suspension-oblivious
  schedule by inflating costs (works with JLDP policies and non-unique priorities)
- Formalize suspension-oblivious FP RTA using the reduction
- Add implementation of a concrete suspension-aware scheduler
- Test suspension-oblivious FP RTA with an actual task set
- Add simpler definition for JLFP policies
- Generalize busy interval lemmas from FP to JLFP scheduling

This commit contains several updates related to uniprocessor scheduling.

- Basic definitions of uniprocessor scheduling (see model/uni)
- Definitions of worload and service for generic sets of jobs (see service.v and workload.v in model/uni)
- Definitions and lemmas about busy intervals (see model/uni/basic/busy_interval.v)
- Definition of an arrival bound for sporadic tasks (see model/arrival_bounds.v)
- Definitions and correctness proofs of the RTA for FP scheduling
  (also works with non-unique priorities and arbitrary deadlines, but gives pessimistic bounds)
- Implementation of the FP RTA to check for contradictory assumptions

In addition, we have also defined partitioned scheduling and proven how it relates
with uniprocessor (see model/partitioned).