{A} (f : A -> A) p a : pos_iter f (pos_succ p) a = pos_iter f p (f a). Proof. revert p f a. srapply pos_peano_ind. 1: hnf; intros; trivial. hnf; intros p q f a. refine (_ @ _ @ _^). 1,3: unfold pos_iter; by rewrite pos_peano_rec_beta_pos_succ. apply ap. apply q. Qed.
Require Import Basics.Overture Basics.Tactics. Require Import Pos.Core.