proposition: Fact iter_swap x n : iter (f x) n = f (iter x n).
proof: Proof. change (iter (f x) n) with (iter x (1+n)). rewrite Nat.add_comm, iter_plus; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)