proposition: Lemma steps_k_monotone {k x} k' : steps k x = None -> k <= k' -> steps k' x = None.
proof: Proof. move=> Hk ?. have ->: k' = k + (k' - k) by lia. by rewrite steps_plus' Hk. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun