proposition: Theorem inj_iter p {A} (f:A->A) (x:A) : Pos.iter f x p = nat_rect _ x (fun _ => f) (to_nat p).
proof: Proof. induction p as [|p IHp] using peano_ind. - trivial. - intros. rewrite inj_succ, iter_succ. simpl. f_equal. apply IHp. Qed.
imports: BinPos PeanoNat