proposition: Lemma path_S_last {k x} : path (S k) x = (path k x) ++ [steps k x].
proof: Proof. by rewrite /path seq_S map_app. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun