diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /theories/Reals/AltSeries.v | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/AltSeries.v')
| -rw-r--r-- | theories/Reals/AltSeries.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index 952853a86..cccc8ceec 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -69,7 +69,7 @@ Lemma CV_ALT_step2 : forall (Un:nat -> R) (N:nat), Un_decreasing Un -> positivity_seq Un -> - sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * N)) <= 0. + sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * N)) <= 0. Proof. intros; induction N as [| N HrecN]. simpl in |- *; unfold tg_alt in |- *; simpl in |- *; rewrite Rmult_1_r. @@ -101,7 +101,7 @@ Qed. Lemma CV_ALT_step3 : forall (Un:nat -> R) (N:nat), Un_decreasing Un -> - positivity_seq Un -> sum_f_R0 (fun i:nat => tg_alt Un (S i)) N <= 0. + positivity_seq Un -> sum_f_R0 (fun i:nat => tg_alt Un (S i)) N <= 0. Proof. intros; induction N as [| N HrecN]. simpl in |- *; unfold tg_alt in |- *; simpl in |- *; rewrite Rmult_1_r. @@ -184,7 +184,7 @@ Proof. rewrite H12; apply H7; assumption. rewrite Rabs_Ropp; unfold tg_alt in |- *; rewrite Rabs_mult; rewrite pow_1_abs; rewrite Rmult_1_l; unfold Rminus in H6; - rewrite Ropp_0 in H6; rewrite <- (Rplus_0_r (Un (S n))); + rewrite Ropp_0 in H6; rewrite <- (Rplus_0_r (Un (S n))); apply H6. unfold ge in |- *; apply le_trans with n. apply le_trans with N; [ unfold N in |- *; apply le_max_r | assumption ]. @@ -246,7 +246,7 @@ Proof. apply CV_ALT_step1; assumption. assumption. unfold Un_cv in |- *; unfold R_dist in |- *; unfold Un_cv in H1; - unfold R_dist in H1; intros. + unfold R_dist in H1; intros. elim (H1 eps H2); intros. exists x; intros. apply H3. @@ -254,20 +254,20 @@ Proof. apply le_trans with n. assumption. assert (H5 := mult_O_le n 2). - elim H5; intro. + elim H5; intro. cut (0%nat <> 2%nat); [ intro; elim H7; symmetry in |- *; assumption | discriminate ]. assumption. apply le_n_Sn. unfold Un_cv in |- *; unfold R_dist in |- *; unfold Un_cv in H1; - unfold R_dist in H1; intros. + unfold R_dist in H1; intros. elim (H1 eps H2); intros. exists x; intros. apply H3. unfold ge in |- *; apply le_trans with n. assumption. assert (H5 := mult_O_le n 2). - elim H5; intro. + elim H5; intro. cut (0%nat <> 2%nat); [ intro; elim H7; symmetry in |- *; assumption | discriminate ]. assumption. |