proposition: Lemma steps_sub {i j x y z} : steps i x = Some y -> steps j x = Some z -> i <= j -> steps (j-i) y = Some z.
proof: Proof. move=> Hi + ?. rewrite [in steps j x](ltac:(lia) : j = i + (j - i)). by rewrite steps_plus' Hi. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun