From b897f00cfc062521f8e4aab5216a42a69ca5cede Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 9 Nov 2018 15:39:43 +0100
Subject: [PATCH] Add `Nat_iter_add`.

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

diff --git a/theories/numbers.v b/theories/numbers.v
index b577e015..ef754a31 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -92,7 +92,11 @@ Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
 Lemma Nat_iter_S {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
 Proof. done. Qed.
 Lemma Nat_iter_S_r {A} n (f: A → A) x : Nat.iter (S n) f x = Nat.iter n f (f x).
-Proof. induction n; f_equal/=; auto. Qed.
+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_ind {A} (P : A → Prop) f x k :
   P x → (∀ y, P y → P (f y)) → P (Nat.iter k f x).
 Proof. induction k; simpl; auto. Qed.
-- 
GitLab