add some simple prefix facts

Add a few straightforward facts about schedules with an identical shared prefix and use these facts to make the EDF optimality proof a bit nicer.

If there are no style complaints etc., I'll merge this shortly.

CC: @mmaida @sbozhko @pointoflight