From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 theories/Reals/Rprod.v | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'theories/Reals/Rprod.v')

diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 2113cc8f..bb3df6bb 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rprod.v 10146 2007-09-27 12:28:12Z herbelin $ i*)
+(*i $Id$ i*)
 
 Require Import Compare.
 Require Import Rbase.
@@ -17,7 +17,7 @@ Require Import Binomial.
 Open Local Scope R_scope.
 
 (** TT Ak; 0<=k<=N *)
-Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) {struct N} : R :=
+Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R :=
   match N with
     | O => f O
     | S p => prod_f_R0 f p * f (S p)
@@ -43,7 +43,7 @@ Proof.
   rewrite Hrecn; [ ring | assumption ].
   omega.
   omega.
-Qed. 
+Qed.
 
 (**********)
 Lemma prod_SO_pos :
@@ -80,9 +80,9 @@ Qed.
 
 (** Application to factorial *)
 Lemma fact_prodSO :
-  forall n:nat, INR (fact n) = prod_f_R0 (fun k:nat => 
-     (match (eq_nat_dec k 0) with 
-          | left   _ => 1%R 
+  forall n:nat, INR (fact n) = prod_f_R0 (fun k:nat =>
+     (match (eq_nat_dec k 0) with
+          | left   _ => 1%R
           | right _ => INR k
                         end)) n.
 Proof.
@@ -102,7 +102,7 @@ Proof.
   replace (S (S (2 * n0))) with (2 * n0 + 2)%nat; [ idtac | ring ].
   replace (S n0) with (n0 + 1)%nat; [ idtac | ring ].
   ring.
-Qed. 
+Qed.
 
 (** We prove that (N!)^2<=(2N-k)!*k! forall k in [|O;2N|] *)
 Lemma RfactN_fact2N_factk :
@@ -112,7 +112,7 @@ Lemma RfactN_fact2N_factk :
 Proof.
   assert (forall (n:nat), 0 <= (if eq_nat_dec n 0 then 1 else INR n)).
   intros; case (eq_nat_dec n 0); auto with real.
-  assert (forall (n:nat), (0 < n)%nat ->  
+  assert (forall (n:nat), (0 < n)%nat ->
      (if eq_nat_dec n 0 then 1 else INR n) = INR n).
   intros n; case (eq_nat_dec n 0); auto with real.
   intros; absurd (0 < n)%nat; omega.
@@ -125,7 +125,7 @@ Proof.
   rewrite Rmult_assoc; apply Rmult_le_compat_l.
   apply prod_SO_pos; intros; auto.
   replace (2 * N - k - N-1)%nat with (N - k-1)%nat.
-  rewrite Rmult_comm; rewrite (prod_SO_split 
+  rewrite Rmult_comm; rewrite (prod_SO_split
         (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) N k).
   apply Rmult_le_compat_l.
   apply prod_SO_pos; intros; auto.
@@ -138,14 +138,14 @@ Proof.
   assumption.
   omega.
   omega.
-  rewrite <- (Rmult_comm (prod_f_R0 (fun l:nat => 
+  rewrite <- (Rmult_comm (prod_f_R0 (fun l:nat =>
           if eq_nat_dec l 0 then 1 else INR l) k));
-    rewrite (prod_SO_split (fun l:nat => 
+    rewrite (prod_SO_split (fun l:nat =>
           if eq_nat_dec l 0 then 1 else INR l) k N).
   rewrite Rmult_assoc; apply Rmult_le_compat_l.
   apply prod_SO_pos; intros; auto.
   rewrite Rmult_comm;
-    rewrite (prod_SO_split (fun l:nat => 
+    rewrite (prod_SO_split (fun l:nat =>
           if eq_nat_dec l 0 then 1 else INR l) N (2 * N - k)).
   apply Rmult_le_compat_l.
   apply prod_SO_pos; intros; auto.
@@ -160,7 +160,7 @@ Proof.
   omega.
   assumption.
   omega.
-Qed. 
+Qed.
 
 
 (**********)
-- 
cgit v1.2.3