From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Arith/PeanoNat.v | 40 +++++++++++++++++++++++++++++++---------
 1 file changed, 31 insertions(+), 9 deletions(-)

(limited to 'theories/Arith/PeanoNat.v')

diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
index e3240bb7..bc58995f 100644
--- a/theories/Arith/PeanoNat.v
+++ b/theories/Arith/PeanoNat.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
@@ -313,7 +315,7 @@ Import Private_Parity.
 
 Lemma even_spec : forall n, even n = true <-> Even n.
 Proof.
- fix 1.
+ fix even_spec 1.
   destruct n as [|[|n]]; simpl.
   - split; [ now exists 0 | trivial ].
   - split; [ discriminate | intro H; elim (Even_1 H) ].
@@ -323,7 +325,7 @@ Qed.
 Lemma odd_spec : forall n, odd n = true <-> Odd n.
 Proof.
  unfold odd.
- fix 1.
+ fix odd_spec 1.
   destruct n as [|[|n]]; simpl.
   - split; [ discriminate | intro H; elim (Odd_0 H) ].
   - split; [ now exists 0 | trivial ].
@@ -471,7 +473,7 @@ Notation "( x | y )" := (divide x y) (at level 0) : nat_scope.
 
 Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b).
 Proof.
- fix 1.
+ fix gcd_divide 1.
  intros [|a] b; simpl.
  split.
   now exists 0.
@@ -500,7 +502,7 @@ Qed.
 
 Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).
 Proof.
- fix 1.
+ fix gcd_greatest 1.
  intros [|a] b; simpl; auto.
  fold (b mod (S a)).
  intros c H H'. apply gcd_greatest; auto.
@@ -534,7 +536,7 @@ Qed.
 Lemma le_div2 n : div2 (S n) <= n.
 Proof.
  revert n.
- fix 1.
+ fix le_div2 1.
  destruct n; simpl; trivial. apply lt_succ_r.
  destruct n; [simpl|]; trivial. now constructor.
 Qed.
@@ -724,6 +726,26 @@ Definition shiftr_spec a n m (_:0<=m) := shiftr_specif a n m.
 
 Include NExtraProp.
 
+(** Properties of tail-recursive addition and multiplication *)
+
+Lemma tail_add_spec n m : tail_add n m = n + m.
+Proof.
+ revert m. induction n as [|n IH]; simpl; trivial.
+ intros. now rewrite IH, add_succ_r.
+Qed.
+
+Lemma tail_addmul_spec r n m : tail_addmul r n m = r + n * m.
+Proof.
+ revert m r. induction n as [| n IH]; simpl; trivial.
+ intros. rewrite IH, tail_add_spec.
+ rewrite add_assoc. f_equal. apply add_comm.
+Qed.
+
+Lemma tail_mul_spec n m : tail_mul n m = n * m.
+Proof.
+ unfold tail_mul. now rewrite tail_addmul_spec.
+Qed.
+
 End Nat.
 
 (** Re-export notations that should be available even when
-- 
cgit v1.2.3