proposition: Lemma inc_value_mod {M : Cm1} {p: Config} : value p < value (step M p) -> exists t, nth_error M (state p) = Some t /\ ((value p) mod ((snd t)+1) = 0).
proof: Proof. rewrite /step. move: p => [i [|c]] /=; first by lia. case: (nth_error M i) => /=; last by lia. move=> [j n]. move Hr: (S c mod (n + 1)) => [|r] /=; last by lia. move=> _. by exists (j, n). Qed.
imports: List PeanoNat BinNat Lia Undecidability.CounterMachines.CM1 ssreflect ssrbool ssrfun