proposition: Lemma steps_loop_mod {K x k} : steps (S K) x = Some x -> steps k x = steps (k mod (S K)) x.
proof: Proof. rewrite [in steps k x](Nat.div_mod_eq k (S K)). move: (k mod (S K)) => k' Hx. elim: (k / S K). - congr steps. lia. - move=> n IH. have ->: S K * S n + k' = S K + (S K * n + k') by lia. by rewrite steps_plus' Hx. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun