diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-26 14:23:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-26 14:50:12 +0200 |
| commit | 55e46598fac67157a5b2c820be621d254581b888 (patch) | |
| tree | 61db2f9a76b3bb55c5fc0131be9600227efc31c2 /theories/Reals/SeqSeries.v | |
| parent | 68d60b7c33b11ad452eca3d2a7ec320963064a9d (diff) | |
Deactivate the "Standard Propositions Naming" flag, source of a lot of
incompatibilities, at least until the check of compilation of contribs
succeeds more often.
Incidentally adapted some proofs in Reals which were not agnostic
relatively to whether the option is on or off.
Diffstat (limited to 'theories/Reals/SeqSeries.v')
| -rw-r--r-- | theories/Reals/SeqSeries.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index fb0c171ad..fc143ce71 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -229,7 +229,7 @@ Proof. do 2 rewrite <- Rplus_assoc; do 2 rewrite Rplus_opp_r; do 2 rewrite Rplus_0_l; do 2 rewrite Rabs_Ropp; repeat rewrite Rabs_right. apply sum_Rle; intros. - elim (H (S n + n0)%nat); intros. + elim (H (S n + n0)%nat); intros H7 H8. apply H8. apply Rle_ge; apply cond_pos_sum; intro. elim (H (S n + n0)%nat); intros. @@ -246,7 +246,7 @@ Proof. do 2 rewrite Rplus_assoc; do 2 rewrite Rplus_opp_l; do 2 rewrite Rplus_0_r; repeat rewrite Rabs_right. apply sum_Rle; intros. - elim (H (S m + n0)%nat); intros; apply H8. + elim (H (S m + n0)%nat); intros H7 H8; apply H8. apply Rle_ge; apply cond_pos_sum; intro. elim (H (S m + n0)%nat); intros. apply Rle_trans with (An (S m + n0)%nat); assumption. |