(n : nat) {A} (f : A -> A) (P : A -> Type) : (forall x, P x -> P (f x)) -> forall x, P x -> P (nat_iter n f x). Proof. simple_induction n n IHn; simpl; trivial. intros Hf x Hx. apply Hf, IHn; trivial. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids