Initial service and completion facts
To get started on #40 (closed) and #41, I've begun to convert some lemmas from /model/schedule/uni/schedule.v to facts files.
This is not yet complete yet in the sense that there are more lemmas in uni/schedule.v that still need to be converted, but it's a start. Maxime, Sergey, please have a look and let me know if this works.
Is this the right place for the _facts files?
Note that, while I've simplified some proofs (and most had to be fixed in some way), I've tried to reuse as much of the existing proofs as possible.