proposition: Lemma config_weight_run_monotone {M: Cm1} {x: Config} {n: nat} : not (halting M (Nat.iter n (step M) x)) -> config_weight M x < config_weight M (Nat.iter (1+n) (step M) x).
proof: Proof. elim: n; first by move /config_weight_step_monotone. move=> n IH HSn. have /IH : not (halting M (Nat.iter n (step M) x)). { move=> Hn. apply: HSn. move: Hn. apply: halting_monotone. by lia. } have := config_weight_step_monotone HSn. move=> /=. by lia. Qed.
imports: List PeanoNat BinNat Lia Undecidability.CounterMachines.CM1 ssreflect ssrbool ssrfun