proposition: Lemma step_value_monotone (M : Cm1) (x: Config) : value x <= value (step M x).
proof: Proof. move: x => [p [|c]] /=; first by lia. case: (nth_error M p) => /=; last by lia. move=> [j n]. move Hr: (S c mod (n + 1)) => [|r] /=; last by lia. have := mod_frac_lt Hr. move=> /=. by lia. Qed.
imports: List PeanoNat BinNat Lia Undecidability.CounterMachines.CM1 ssreflect ssrbool ssrfun