summaryrefslogtreecommitdiff
path: root/theories/Reals/Exp_prop.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
commit55ce117e8083477593cf1ff2e51a3641c7973830 (patch)
treea82defb4105f175c71b0d13cae42831ce608c4d6 /theories/Reals/Exp_prop.v
parent208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff)
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'theories/Reals/Exp_prop.v')
-rw-r--r--theories/Reals/Exp_prop.v22
1 files changed, 11 insertions, 11 deletions
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 5dafec83..beb4b744 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Exp_prop.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Exp_prop.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -87,7 +87,7 @@ Proof.
reflexivity.
replace (2 * S N)%nat with (S (S (2 * N))).
simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
- ring_nat.
+ ring.
Qed.
Lemma div2_S_double : forall N:nat, div2 (S (2 * N)) = N.
@@ -96,7 +96,7 @@ Proof.
reflexivity.
replace (2 * S N)%nat with (S (S (2 * N))).
simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
- ring_nat.
+ ring.
Qed.
Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat.
@@ -367,7 +367,7 @@ Proof.
apply le_trans with (pred N).
apply H0.
apply le_pred_n.
- rewrite H4; ring_nat.
+ rewrite H4; ring.
cut (S N = (2 * S N0)%nat).
intro.
replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))).
@@ -388,7 +388,7 @@ Proof.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
- rewrite H4; ring_nat.
+ rewrite H4; ring.
unfold C, Rdiv in |- *.
rewrite (Rmult_comm (INR (fact (S N)))).
rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
@@ -494,7 +494,7 @@ Proof.
simpl in |- *.
pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
apply Rlt_0_1.
- ring_nat.
+ ring.
unfold Rsqr in |- *; apply prod_neq_R0; apply INR_fact_neq_0.
unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; discriminate.
assert (H0 := even_odd_cor N).
@@ -515,7 +515,7 @@ Proof.
replace (S (S (2 * N0))) with (2 * S N0)%nat.
do 2 rewrite div2_double.
reflexivity.
- ring_nat.
+ ring.
apply S_pred with 0%nat; apply H.
Qed.
@@ -585,8 +585,8 @@ Proof.
apply (fun m n p:nat => mult_le_compat_l p n m).
replace (2 * S N1)%nat with (S (S (2 * N1))).
apply le_n_Sn.
- ring_nat.
- ring_nat.
+ ring.
+ ring.
reflexivity.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
@@ -623,7 +623,7 @@ Proof.
replace (2 * N1)%nat with (S (S (2 * pred N1))).
reflexivity.
pattern N1 at 2 in |- *; replace N1 with (S (pred N1)).
- ring_nat.
+ ring.
symmetry in |- *; apply S_pred with 0%nat; apply H8.
apply INR_lt.
apply Rmult_lt_reg_l with (INR 2).
@@ -641,7 +641,7 @@ Proof.
rewrite div2_double.
replace (2 * S N1)%nat with (S (S (2 * N1))).
apply le_n_Sn.
- ring_nat.
+ ring.
reflexivity.
apply le_trans with (max (2 * S N0) 2).
apply le_max_l.