Integrate rt_eauto into done (hence by and //)

analysis/abstract/abstract_rta.v

analysis/abstract/busy_interval.v

analysis/abstract/definitions.v

analysis/abstract/ideal/abstract_rta.v

analysis/abstract/ideal/abstract_seq_rta.v

analysis/abstract/ideal/iw_instantiation.v

analysis/abstract/lower_bound_on_service.v

analysis/abstract/search_space.v

analysis/definitions/busy_interval.v

analysis/facts/behavior/arrivals.v

analysis/facts/busy_interval/carry_in.v

analysis/facts/busy_interval/ideal/busy_interval.v

analysis/facts/busy_interval/ideal/carry_in.v

analysis/facts/busy_interval/ideal/hep_job_scheduled.v

analysis/facts/busy_interval/ideal/inequalities.v

analysis/facts/busy_interval/ideal/priority_inversion.v

...is/facts/busy_interval/ideal/priority_inversion_bounded.v

...cts/busy_interval/ideal/priority_inversion_bounded_jlfp.v

analysis/facts/edf_definitions.v

analysis/facts/hyperperiod.v