From 70a21632aac4f90342a0dddbe594b7b6b5049d18 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Feb 2021 12:11:53 +0100
Subject: [PATCH] add Nat_iter_mul

---
 theories/numbers.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/numbers.v b/theories/numbers.v
index b936f22b..750647cd 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -100,6 +100,12 @@ Proof. induction n; by f_equal/=. Qed.
 Lemma Nat_iter_add {A} n1 n2 (f : A → A) x :
   Nat.iter (n1 + n2) f x = Nat.iter n1 f (Nat.iter n2 f x).
 Proof. induction n1; by f_equal/=. Qed.
+Lemma Nat_iter_mul {A} n1 n2 (f : A → A) x :
+  Nat.iter (n1 * n2) f x = Nat.iter n1 (Nat.iter n2 f) x.
+Proof.
+  intros. induction n1 as [|n1 IHn1]; [done|].
+  simpl. by rewrite Nat_iter_add, IHn1.
+Qed.
 
 Lemma Nat_iter_ind {A} (P : A → Prop) f x k :
   P x → (∀ y, P y → P (f y)) → P (Nat.iter k f x).
-- 
GitLab