proposition: Theorem nat_iter_invariant (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: Proof. simple_induction n n IHn; simpl; trivial. intros Hf x Hx. apply Hf, IHn; trivial. Defined.
imports: Basics Types Basics.Nat HoTT.DProp