move misplaced code out of `prosa.analysis.facts.busy_window`

- The busy_window.v file still depends on the ideal uniprocessor
  assumption, so move it to the ideal submodule.

- The priority_inversion.v file has nothing to do with busy windows,
  so move it to the prosa.analysis.facts.priority module.

- Move a trivial quiet-time lemma from carry_in.v to quiet_time.v.

Much cleanup of the ideal submodule remains to be done...

See also: #112