Simplify bertogna fp

bertogna_edf_theory.v

-Require Import Vbase task job task_arrival schedule platform
+Require Import Vbase task job task_arrival schedule platform interference
         workload workload_bound schedulability priority response_time
         bertogna_fp_theory util_divround util_lemmas
         ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
@@ -6,7 +6,7 @@ Require Import Vbase task job task_arrival schedule platform
 Module ResponseTimeAnalysisEDF.
 
   Export Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime
-         Priority SporadicTaskArrival ResponseTimeAnalysis WorkloadBound.
+         Priority SporadicTaskArrival WorkloadBound ResponseTimeAnalysisFP.
 
   Section InterferenceBoundEDF.
 

bertogna_fp_comp.v

@@ -4,7 +4,7 @@ Require Import Vbase schedule bertogna_fp_theory util_divround util_lemmas
 
 Module ResponseTimeIterationFP.
 
-  Import Schedule ResponseTimeAnalysis WorkloadBound.
+  Import Schedule ResponseTimeAnalysisFP WorkloadBound.
 
   Section Analysis.
     

guan_fp_comp.v

 Require Import Vbase job task schedule task_arrival priority workload_jitter
-               workload_guan guan_fp_theory util_divround util_lemmas
+               workload_guan interference response_time schedulability platform guan_fp_theory util_divround util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
 
 Module ResponseTimeIterationFPGuan.
 
-  Import Job ScheduleOfTaskWithJitter SporadicTaskset SporadicTaskArrival Priority WorkloadWithJitter ResponseTimeAnalysisGuan WorkloadBoundGuan.
+  Import Job ScheduleOfTaskWithJitter SporadicTaskset SporadicTaskArrival Priority
+         WorkloadWithJitter ResponseTimeAnalysisGuan WorkloadBoundGuan Interference
+         Platform Schedulability ResponseTime. 
 
   Section Analysis.
     

guan_fp_theory.v

@@ -6,7 +6,7 @@ Require Import Vbase task job task_arrival schedule platform workload
 Module ResponseTimeAnalysisGuan.
 
   Import Job SporadicTaskset ScheduleOfTaskWithJitter Schedulability ResponseTime Priority SporadicTaskArrival Interference Platform WorkloadBoundGuan.
-  Export Workload ResponseTimeAnalysis.
+  Export Workload.
 
   Section InterferenceBoundGuan.