proposition: Lemma pos_iter_succ_r {A} (f : A -> A) p a : pos_iter f (pos_succ p) a = pos_iter f p (f a).
proof: 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.
imports: Basics.Overture Basics.Tactics Pos.Core