diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-03 17:15:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-04 18:42:22 +0200 |
| commit | e1e0f4f7f3c549fd3d5677b67c6b13ed687e6f12 (patch) | |
| tree | 70d40db0a8bb6378bb97d9c7c72567045bd4bd78 /theories/Reals/PartSum.v | |
| parent | 6c9e2ded8fc093e42902d008a883b6650533d47f (diff) | |
Make standard library independent of the names generated by
induction/elim over a dependent elimination principle for Prop
arguments.
Diffstat (limited to 'theories/Reals/PartSum.v')
| -rw-r--r-- | theories/Reals/PartSum.v | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 10c3327f2..d559efbce 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -180,12 +180,9 @@ Proof. replace (S (S (pred N))) with (S N). rewrite (HrecN H1); ring. rewrite H2; simpl; reflexivity. - assert (H2 := O_or_S N). - elim H2; intros. - elim a; intros. - rewrite <- p. + destruct (O_or_S N) as [(m,<-)|<-]. simpl; reflexivity. - rewrite <- b in H1; elim (lt_irrefl _ H1). + elim (lt_irrefl _ H1). rewrite H1; simpl; reflexivity. inversion H. right; reflexivity. @@ -395,9 +392,7 @@ Proof. (sum_f_R0 (fun i:nat => Rabs (An i)) m)). assumption. apply H1; assumption. - assert (H4 := lt_eq_lt_dec n m). - elim H4; intro. - elim a; intro. + destruct (lt_eq_lt_dec n m) as [[ | -> ]|]. rewrite (tech2 An n m); [ idtac | assumption ]. rewrite (tech2 (fun i:nat => Rabs (An i)) n m); [ idtac | assumption ]. unfold R_dist. @@ -418,7 +413,6 @@ Proof. apply Rle_ge. apply cond_pos_sum. intro; apply Rabs_pos. - rewrite b. unfold R_dist. unfold Rminus; do 2 rewrite Rplus_opp_r. rewrite Rabs_R0; right; reflexivity. @@ -451,8 +445,7 @@ Lemma cv_cauchy_1 : { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } -> Cauchy_crit_series An. Proof. - intros An X. - elim X; intros. + intros An (x,p). unfold Un_cv in p. unfold Cauchy_crit_series; unfold Cauchy_crit. intros. |