Prove one of the cheats in replCorrect using the no-output result

Also required a few more divergence-related results, since
code_executes_ok is defined in terms of NRC of an arbitrary n.

New result says that if the clock decreases by n, then at least n steps
must have been taken.