{A} (f : A -> A) p a : pos_iter f (pos_succ p) a = f (pos_iter f p a). Proof. unfold pos_iter. by rewrite pos_peano_rec_beta_pos_succ. Qed.
Require Import Basics.Overture Basics.Tactics. Require Import Pos.Core.