proposition: Lemma iter_mul {A} n1 n2 (f : A → A) x : Nat.iter (n1 * n2) f x = Nat.iter n1 (Nat.iter n2 f) x.
proof: Proof. intros. induction n1 as [|n1 IHn1]; [done|]. simpl. by rewrite iter_add, IHn1. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)