refactoring: port initial service and completion lemmas

...from model/schedule/uni/schedule.v.

To simplify some of the rather long proofs in the original file, the patch introduces a bunch of small and simple rewriting and helper lemmas that we previously lacked, but that we *should* have to avoid having to reason at the level of sslreflect "big" operators in every lemma.