EDF optimality proof should derive from its weaker version

In file analysis/edf/optimality.v