proposition: Lemma value_monotone {M : Cm1} {x: Config} {n m: nat} : n <= m -> value (Nat.iter n (step M) x) <= value (Nat.iter m (step M) x).
proof: Proof. move=> ?. have ->: (m = n + (m - n)) by lia. rewrite iter_plus. by apply: run_value_monotone. Qed.
imports: List PeanoNat BinNat Lia Undecidability.CounterMachines.CM1 ssreflect ssrbool ssrfun