diff options
Diffstat (limited to 'theories/Reals/ArithProp.v')
| -rw-r--r-- | theories/Reals/ArithProp.v | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index cfc74fc4..c4e410ed 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -105,14 +105,14 @@ Proof. exists (x - IZR k0 * y). split. ring. - unfold k0; case (Rcase_abs y); intro. + unfold k0; case (Rcase_abs y) as [Hlt|Hge]. assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl; unfold Rminus. replace (- ((1 + - IZR (up (x / - y))) * y)) with ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ]. split. apply Rmult_le_reg_l with (/ - y). - apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact r. + apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact Hlt. rewrite Rmult_0_r; rewrite (Rmult_comm (/ - y)); rewrite Rmult_plus_distr_r; rewrite <- Ropp_inv_permute; [ idtac | assumption ]. rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse; @@ -125,14 +125,14 @@ Proof. (- (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). - apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact r. + rewrite (Rabs_left _ Hlt); apply Rmult_lt_reg_l with (/ - y). + apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact Hlt. rewrite <- Rinv_l_sym. rewrite (Rmult_comm (/ - y)); rewrite Rmult_plus_distr_r; rewrite <- Ropp_inv_permute; [ idtac | assumption ]. rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ]; - apply Rplus_lt_reg_r with (IZR (up (x / - y)) - 1). + apply Rplus_lt_reg_l with (IZR (up (x / - y)) - 1). replace (IZR (up (x / - y)) - 1 + 1) with (IZR (up (x / - y))); [ idtac | ring ]. replace (IZR (up (x / - y)) - 1 + (- (x * / y) + - (IZR (up (x / - y)) - 1))) @@ -157,22 +157,21 @@ Proof. (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; exact H2. - rewrite (Rabs_right _ r); apply Rmult_lt_reg_l with (/ y). + rewrite (Rabs_right _ Hge); apply Rmult_lt_reg_l with (/ y). apply Rinv_0_lt_compat; assumption. rewrite <- (Rinv_l_sym _ H); rewrite (Rmult_comm (/ y)); 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); + apply Rplus_lt_reg_l with (IZR (up (x / y)) - 1); 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; intros H2 _; exact H2. - case (total_order_T 0 y); intro. - elim s; intro. + destruct (total_order_T 0 y) as [[Hlt|Heq]|Hgt]. assumption. - elim H; symmetry ; exact b. - assert (H1 := Rge_le _ _ r); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 r0)). + elim H; symmetry ; exact Heq. + apply Rge_le in Hge; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hge Hgt)). Qed. Lemma tech8 : forall n i:nat, (n <= S n + i)%nat. |