Monotone Coupling from the Past Correctness Theorem