proposition: Lemma iter_nat_plus : forall (p q : nat) (x : A), iter_nat (p + q) x = iter_nat p (iter_nat q x).
proof: Proof. induction q. now rewrite Nat.add_0_r. intros x. rewrite <- plus_n_Sm. apply IHq. Qed.
imports: Coq(ZArith Lia Zquot)