proposition: Lemma shift_path_a K p a b : path (K+1) (p, (K+a, b)) = map (fun oy => if oy is Some (p', (a', b')) then Some (p', (a'+a, b')) else None) (path (K+1) (p, (K, b))).
proof: Proof. rewrite /path map_map. apply: map_ext_in => k /in_seq ?. apply: shift_steps_a. lia. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun