proposition: Lemma iter_plus {X: Type} {f: X -> X} {x: X} {n m: nat} : Nat.iter (n + m) f x = Nat.iter m f (Nat.iter n f x).
proof: Proof. by rewrite Nat.add_comm /Nat.iter nat_rect_plus. Qed.
imports: List PeanoNat BinNat Lia Undecidability.CounterMachines.CM1 ssreflect ssrbool ssrfun