proposition: Lemma iter_pos_nat : forall (p : positive) (x : A), iter_pos f p x = iter_nat (Pos.to_nat p) x.
proof: Proof. induction p ; intros x. rewrite Pos2Nat.inj_xI. simpl. rewrite Nat.add_0_r. rewrite iter_nat_plus. rewrite (IHp (f x)). apply IHp. rewrite Pos2Nat.inj_xO. simpl. rewrite Nat.add_0_r. rewrite iter_nat_plus. rewrite (IHp x). apply IHp. easy. Qed.
imports: Coq(ZArith Lia Zquot)