Reorganize and clean up restructuring.module

This patch series completely re-shuffles how the rt.restructuring.model module is organized. I believe this to be much more logically meaningful and easier to work with in the future.

There are now the following sub-modules:

• model.aggregate: functions on sets of jobs (unchanged)
• model.arrival: arrival models for tasks (unchanged), to be extended with periodic, etc. ...
• model.preemption: the new preemption model for jobs (no mention of tasks)
• model.priority: FP/JFLP/JLDP policies, to be extended with FIFO, RM, DM, ...
• model.processor: processor models and platform properties (unchanged)
• model.readiness: various way to define job_ready (unchanged), to be extended with self-suspensions...
• model.schedule: definitions related to schedules, including priority-driven schedules
• model.task: everything about the task abstraction (except for arrivals, see above)
• model.task.preemption: the new preemption model for tasks

I recommend looking through it here: http://prosa.mpi-sws.org/branches/model-reorg/pretty/tree.html (scroll to the bottom).

@mlesourd @sophie @sbozhko: Please comment if anything sticks out. This organization is of course not set in stone; we can improve it later. So unless there are major concerns, I'd rather go ahead soon and worry about making it perfect in future revisions, as I think it's much better than what we've had so far and it blocks further clean-up work.

Note 1: the comments still need to be cleaned-up and improved; this is something for next week. (Help of course always welcome.)

Note 2: the analysis module will similarly have to be reorganized; this is pending and will be possible only after Sergey is done with the Require cleanup in analysis.

restructuring/model/task/preemption/floating_nonpreemptive.v

 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Export rt.restructuring.model.task.preemption.parameters.
 
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
 (** * Platform for Models with Floating Non-Preemptive Regions *)
 (** In this section, we introduce a set of requirements for function
     [task_max_nonpr_segment], so it is coherent with model with