diff options
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/Alembert.v | 12 | ||||
| -rw-r--r-- | theories/Reals/SeqSeries.v | 4 |
2 files changed, 8 insertions, 8 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index c4416e5d8..c037fdd20 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -472,11 +472,11 @@ Proof. elim Hyp; intros; assumption. elim H3; intros; assumption. apply Rminus_eq_contra. - red; intro. - elim H3; intros. + red; intro H10. + elim H3; intros H11 H12. rewrite H10 in H12; elim (Rlt_irrefl _ H12). - red; intro. - elim H3; intros. + red; intro H10. + elim H3; intros H11 H12. rewrite H10 in H12; elim (Rlt_irrefl _ H12). replace (An (S x0)) with (An (S x0 + 0)%nat). apply (tech6 (fun i:nat => An (S x0 + i)%nat) x). @@ -485,7 +485,7 @@ Proof. elim H3; intros; assumption. intro. cut (forall n:nat, (n >= x0)%nat -> An (S n) < x * An n). - intro. + intro H9. replace (S x0 + S i)%nat with (S (S x0 + i)). apply H9. unfold ge. @@ -507,7 +507,7 @@ Proof. apply Rmult_lt_0_compat. apply H. apply Rinv_0_lt_compat; apply H. - red; intro. + red; intro H10. assert (H11 := H n). rewrite H10 in H11; elim (Rlt_irrefl _ H11). replace (S x0 + 0)%nat with (S x0); [ reflexivity | ring ]. 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. |