As a Coq/sslreflect/Prosa exercise, and to get a feel for the restructured foundation, I've been working on a proof of the classic EDF optimality argument that proceeds by swapping pairs of jobs that violate EDF. While this is not particularly useful (i.e., it's not essential for anything else on our radar at the moment), it's a nice classic result that I'd like to integrate anyway.
As part of this work, I've also cleaned up a few things in the foundation and added some utility lemmas.
Review and feedback would be much appreciated, both on the proof itself and the organization/naming of the files/lemmas/defs. I'm still learning, so if I'm doing something "wrong" or strangely in some proof, please point it out.
As a starting point, the main optimality claim may be found in: rt.restructuring.analysis.edf.optimality.