Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

* rename [step_function] to [unit_growth]
* restructure file

Mariam Vardishvili authored 3 years ago and Björn Brandenburg committed 3 years ago

The lemma [instantiated_busy_interval_equivalent_edf_busy_interval] actually does not depend on EDF.

lemma [count_filter_fun] is equivalent to ssreflect's [size_filter]

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

Note that many files have changed; however, this is due to the fact that some of the lemmas in nat.v have been renamed or removed.

Can't rely on arg_maxnP just yet.

This change breaks compatibility with mathcomp < 1.10.

Move everything into the new namespace starting with 'prosa' rather
than the bland 'rt'.

File preemption.util is renamed and moved to
util.nondecreasing. The new util file can be used
in both the old Prosa and the new Prosa.