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/Ranalysis3.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/Ranalysis3.v')
| -rw-r--r-- | theories/Reals/Ranalysis3.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index cb48a26b8..3de97ba90 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -213,7 +213,7 @@ Proof. apply Rabs_pos_lt; unfold Rdiv, Rsqr in |- *; repeat rewrite Rmult_assoc; repeat apply prod_neq_R0. red in |- *; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6). - assumption. + assumption. assumption. apply Rinv_neq_0_compat; repeat apply prod_neq_R0; [ discrR | discrR | discrR | assumption ]. @@ -380,7 +380,7 @@ Proof. unfold Rdiv, Rsqr in |- *. repeat rewrite Rinv_mult_distr; try assumption. repeat apply prod_neq_R0; try assumption. - red in |- *; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6). + red in |- *; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6). apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; discrR. @@ -408,14 +408,14 @@ Proof. unfold Rsqr, Rdiv in |- *. repeat rewrite Rinv_mult_distr; try assumption || discrR. repeat apply prod_neq_R0; try assumption. - red in |- *; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6). + red in |- *; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6). apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; assumption. apply Rinv_neq_0_compat; assumption. apply prod_neq_R0; [ discrR | assumption ]. - red in |- *; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6). + red in |- *; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6). apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; discrR. @@ -519,7 +519,7 @@ Proof. repeat apply Rmin_pos. apply (cond_pos eps_f2). elim H3; intros; assumption. - apply (cond_pos alp_f1d). + apply (cond_pos alp_f1d). apply (cond_pos alp_f2d). elim H11; intros; assumption. apply Rabs_pos_lt. @@ -776,7 +776,7 @@ Proof. Qed. Lemma derive_pt_div : - forall (f1 f2:R -> R) (x:R) (pr1:derivable_pt f1 x) + forall (f1 f2:R -> R) (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x) (na:f2 x <> 0), derive_pt (f1 / f2) x (derivable_pt_div _ _ _ pr1 pr2 na) = (derive_pt f1 x pr1 * f2 x - derive_pt f2 x pr2 * f1 x) / Rsqr (f2 x). |