(n m : nat) {A} (f : A -> A) (x : A) : nat_iter (n + m) f x = nat_iter n f (nat_iter m f x). Proof. simple_induction n n IHn; simpl; trivial. exact (ap f IHn). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids