add definition of a job's (precise) finish time

This small MR defines the notion of a job's "finish time". To get around the problem that a job may never finish, we reuse ssreflect's ex_minn facility to define finish_time under the assumption that the job eventually finishes.

This has no immediate users. The main point is to show that it can be done (and as an example for Lars).

Rendered spec: https://prosa.mpi-sws.org/branches/wip-finish-time/pretty/prosa.analysis.definitions.finish_time.html