proposition: Lemma In_None_pathE k x : In None (path k x) -> steps k x = None.
proof: Proof. move=> /In_pathE [k' [?]] /(steps_k_monotone k). apply. lia. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun