proposition: Lemma run_value_monotone (M : Cm1) (x: Config) (n: nat) : value x <= value (Nat.iter n (step M) x).
proof: Proof. elim: n=> /=; first by lia. move=> n IH. have := step_value_monotone M (Nat.iter n (step M) x). by lia. Qed.
imports: List PeanoNat BinNat Lia Undecidability.CounterMachines.CM1 ssreflect ssrbool ssrfun