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/ArithProp.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/ArithProp.v')
| -rw-r--r-- | theories/Reals/ArithProp.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index a5c5ddaf8..f22ff5cb2 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -124,7 +124,7 @@ Proof. rewrite <- Ropp_inv_permute; [ idtac | assumption ]. replace (IZR (up (x * / - y)) - x * - / y + - (- (x * / y) + - (IZR (up (x * / - y)) - 1))) with 1; + (- (x * / y) + - (IZR (up (x * / - y)) - 1))) with 1; [ idtac | ring ]. elim H0; intros _ H1; unfold Rdiv in H1; exact H1. rewrite (Rabs_left _ r); apply Rmult_lt_reg_l with (/ - y). @@ -153,11 +153,11 @@ Proof. rewrite Rmult_0_r; rewrite (Rmult_comm (/ y)); rewrite Rmult_plus_distr_r; rewrite Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ]; - apply Rplus_le_reg_l with (IZR (up (x / y)) - x / y); + apply Rplus_le_reg_l with (IZR (up (x / y)) - x / y); rewrite Rplus_0_r; unfold Rdiv in |- *; replace (IZR (up (x * / y)) - x * / y + (x * / y + (1 - IZR (up (x * / y))))) with - 1; [ idtac | ring ]; elim H0; intros _ H2; unfold Rdiv in H2; + 1; [ idtac | ring ]; elim H0; intros _ H2; unfold Rdiv in H2; exact H2. rewrite (Rabs_right _ r); apply Rmult_lt_reg_l with (/ y). apply Rinv_0_lt_compat; assumption. @@ -165,10 +165,10 @@ Proof. rewrite Rmult_plus_distr_r; rewrite Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ]; apply Rplus_lt_reg_r with (IZR (up (x / y)) - 1); - replace (IZR (up (x / y)) - 1 + 1) with (IZR (up (x / y))); + replace (IZR (up (x / y)) - 1 + 1) with (IZR (up (x / y))); [ idtac | ring ]; replace (IZR (up (x / y)) - 1 + (x * / y + (1 - IZR (up (x / y))))) with - (x * / y); [ idtac | ring ]; elim H0; unfold Rdiv in |- *; + (x * / y); [ idtac | ring ]; elim H0; unfold Rdiv in |- *; intros H2 _; exact H2. case (total_order_T 0 y); intro. elim s; intro. |