diff options
Diffstat (limited to 'theories/Reals/Ranalysis2.v')
| -rw-r--r-- | theories/Reals/Ranalysis2.v | 31 |
1 files changed, 12 insertions, 19 deletions
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 0254218c..7a97ca63 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Rbase. @@ -88,17 +90,11 @@ Proof. right; unfold Rdiv. repeat rewrite Rabs_mult. rewrite Rabs_Rinv; discrR. - replace (Rabs 8) with 8. - replace 8 with 8; [ idtac | ring ]. - rewrite Rinv_mult_distr; [ idtac | discrR | discrR ]. - replace (2 * / Rabs (f2 x) * (Rabs eps * Rabs (f2 x) * (/ 2 * / 4))) with - (Rabs eps * / 4 * (2 * / 2) * (Rabs (f2 x) * / Rabs (f2 x))); - [ idtac | ring ]. - replace (Rabs eps) with eps. - repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption). - ring. - symmetry ; apply Rabs_right; left; assumption. - symmetry ; apply Rabs_right; left; prove_sup. + rewrite (Rabs_pos_eq 8) by now apply IZR_le. + rewrite (Rabs_pos_eq eps). + field. + now apply Rabs_no_R0. + now apply Rlt_le. Qed. Lemma maj_term2 : @@ -429,10 +425,7 @@ Proof. intro; rewrite H11 in H10; assert (H12 := Rmult_lt_compat_l 2 _ _ Hyp H10); rewrite Rmult_1_r in H12; rewrite <- Rinv_r_sym in H12; [ idtac | discrR ]. - cut (IZR 1 < IZR 2). - unfold IZR; unfold INR, Pos.to_nat; simpl; intro; - elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)). - apply IZR_lt; omega. + now apply lt_IZR in H12. unfold Rabs; case (Rcase_abs (/ 2)) as [Hlt|Hge]. assert (Hyp : 0 < 2). prove_sup0. |