diff options
Diffstat (limited to 'theories/Reals/RiemannInt_SF.v')
| -rw-r--r-- | theories/Reals/RiemannInt_SF.v | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 7885d697..ceac021e 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.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. @@ -83,11 +85,10 @@ Proof. cut (x = INR (pred x0)). intro H19; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18; rewrite <- H19; assumption. - rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; replace 1 with (INR 1); - [ idtac | reflexivity ]; rewrite <- minus_INR. - replace (x0 - 1)%nat with (pred x0); - [ reflexivity - | case x0; [ reflexivity | intro; simpl; apply minus_n_O ] ]. + rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; + rewrite <- (minus_INR _ 1). + apply f_equal; + case x0; [ reflexivity | intro; apply sym_eq, minus_n_O ]. induction x0 as [|x0 Hrecx0]. rewrite H8 in H3. rewrite <- INR_IZR_INZ in H3; simpl in H3. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H3)). |