Remove ideal assumption from aRTA-seq and generalize proof [task_IBF -> job_IBF]

Depends on !314 (merged) and !315 (merged)

added 9 commits

• 64f0a3de - add two corollaries about `is_idle` and `scheduled_at`
• 03a263f3 - remove ideal uni-proc assumption from ideal/busy_interval.v
• 3137a998 - remove `ideal.carry_in` (generalize last remaining lemma)
• 9656e4ae - move `busy_interval.ideal.priority_inversion` -> `facts.model.ideal`
• 1b6fef7e - move `busy_interval.ideal.inequalities` -> `abstract.ideal`
• d1d82a50 - remove ideal uni-proc assumption from hep_job_scheduled.v
• d6c052da - remove ideal uni-proc assumption from priority_inversion_bounded.v
• 86834957 - clean up [analysis.facts.busy_interval.carry_in]
• 4023b118 - remove [ideal.processor] proc. model

Compare with previous version

added 4 commits

• 4023b118...8ed55ead - 3 commits from branch RT-PROOFS:master
• 3ecf0248 - remove [ideal.processor] proc. model

Compare with previous version

added 2 commits

• f9383274 - silence warning
• 2d5058f8 - to squash: simplify proof step

Compare with previous version

added 6 commits

• b28492ca - remove [ideal.processor] proc. model
• 152a16d6 - : generalize aRTA seq
• fb853be9 - : close all proofs
• 84eec012 - silence warning
• fe2584ac - make indentation more consistent
• 8d302bca - : clean up

Compare with previous version

added 1 commit

• ecc39fdb - : fix spelling

Compare with previous version

added 4 commits

• 9009b91f - silence warning
• 6598af14 - make indentation more consistent
• 3543bb1d - remove [ideal.processor] proc. model
• c14a4069 - generalize [task_IBF -> job_IBF] proof

Compare with previous version

marked this merge request as ready

changed title from Draft: Remove ideal assumption from aRTA-seq to Remove ideal assumption from aRTA-seq and generalize proof [task_IBF -> job_IBF]

requested review from @proux

assigned to @bbb