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/analysis/abstract/core/abstract_rta.v

-Require Import rt.util.all.
-Require Import rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.definitions.job_properties.
-Require Import rt.restructuring.model.task.concept.
-
-Require Import rt.restructuring.model.preemption.parameter.
-Require Import rt.restructuring.model.task.preemption.parameters.
-
-Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
-Require Import rt.restructuring.analysis.schedulability.
-Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.restructuring.analysis.abstract.core.definitions.
-Require Import rt.restructuring.analysis.abstract.core.reduction_of_search_space.
-Require Import rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold.
+Require Export rt.restructuring.analysis.schedulability.
+Require Export rt.restructuring.analysis.abstract.core.reduction_of_search_space.
+Require Export rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.