proposition: Lemma bounded_monotone {k k' x} : k <= k' -> bounded k x -> bounded k' x.
proof: Proof. move=> ? [L [? ?]]. exists L. split; [lia|done]. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun