proposition: Fact Natiter_S n X (f : X -> X) x : Nat.iter (S n) f x = Nat.iter n f (f x).
proof: Proof. replace (S n) with (n+1) by lia. rewrite Natiter_add; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils pos subcode sss) Undecidability.Synthetic(ReducibilityFacts) Undecidability.TM(SBTM pctm_defs)