Simplify definition of priority inversion

Given the new scheduled_job_at definition, the existing definition of priority_inversion and its decidable counterpart seem too complicated.

Proposal: We should revise priority_inversion and priority_inversion_dec, ideally getting rid of one of them, and base the remaining definition on scheduled_job_at.