From 5c7064e1988fbcdf225f2be658bc3ebd24ef51df Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2017 11:48:35 +0100
Subject: [PATCH] Prove nat_iter_ind.

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

diff --git a/theories/numbers.v b/theories/numbers.v
index 4e27271a..52d0bf1d 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -98,6 +98,9 @@ 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.
+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.
 
 (** * Notations and properties of [positive] *)
 Open Scope positive_scope.
-- 
GitLab