move unused helper lemmas/notations/tactics to rt.classic

classic/analysis/apa/bertogna_edf_comp.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.analysis.apa.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 

classic/analysis/apa/bertogna_edf_theory.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
 Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.response_time
                rt.classic.model.schedule.global.schedulability.

classic/analysis/apa/bertogna_fp_comp.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.analysis.apa.bertogna_fp_theory.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
 

classic/analysis/apa/bertogna_fp_theory.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
 Require Import rt.classic.model.schedule.global.response_time rt.classic.model.schedule.global.schedulability
                rt.classic.model.schedule.global.workload.

classic/analysis/apa/interference_bound.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.schedule.global.basic.schedule.
 Require Import rt.classic.analysis.apa.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

classic/analysis/apa/interference_bound_edf.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
 Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.response_time
                rt.classic.model.schedule.global.schedulability.

classic/analysis/apa/interference_bound_fp.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.priority.
 Require Import rt.classic.model.schedule.global.workload.
 Require Import rt.classic.model.schedule.global.basic.schedule.

classic/analysis/apa/workload_bound.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival.
 Require Import rt.classic.model.schedule.global.response_time rt.classic.model.schedule.global.schedulability
                rt.classic.model.schedule.global.workload.

classic/analysis/global/basic/bertogna_edf_comp.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.analysis.global.basic.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 

classic/analysis/global/basic/bertogna_edf_theory.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival rt.classic.model.priority.
 Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.schedulability
                rt.classic.model.schedule.global.response_time.

classic/analysis/global/basic/bertogna_fp_comp.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.analysis.global.basic.bertogna_fp_theory.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
 

classic/analysis/global/basic/bertogna_fp_theory.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
 Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.schedulability
                rt.classic.model.schedule.global.response_time.

classic/analysis/global/basic/interference_bound.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.schedule.global.basic.schedule.
 Require Import rt.classic.analysis.global.basic.workload_bound.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

classic/analysis/global/basic/interference_bound_edf.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival rt.classic.model.priority.
 Require Import rt.classic.model.schedule.global.response_time rt.classic.model.schedule.global.workload
                rt.classic.model.schedule.global.schedulability.

classic/analysis/global/basic/interference_bound_fp.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.priority.
 Require Import rt.classic.model.schedule.global.workload.
 Require Import rt.classic.model.schedule.global.basic.schedule rt.classic.model.schedule.global.basic.interference.

classic/analysis/global/basic/workload_bound.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.arrival.basic.task rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task_arrival.
 Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.response_time
                rt.classic.model.schedule.global.schedulability.

classic/analysis/global/jitter/bertogna_edf_comp.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.analysis.global.jitter.bertogna_edf_theory.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 

classic/analysis/global/jitter/bertogna_edf_theory.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
 Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.schedulability
                rt.classic.model.schedule.global.response_time.

classic/analysis/global/jitter/bertogna_fp_comp.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.analysis.global.jitter.bertogna_fp_theory.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
 

classic/analysis/global/jitter/bertogna_fp_theory.v

-Require Import rt.util.all.
+Require Import rt.classic.util.all.
 Require Import rt.classic.model.arrival.basic.task rt.classic.model.priority rt.classic.model.arrival.basic.task_arrival.
 Require Import rt.classic.model.schedule.global.workload rt.classic.model.schedule.global.response_time
                rt.classic.model.schedule.global.schedulability.