diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-04-02 10:30:59 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-04-02 10:33:44 +0200 |
| commit | 58bc387700d1fe4856571e8fae5c1761f89adc38 (patch) | |
| tree | e0cf041a35ccbf5315d900e3bf05024bb38c8c96 /theories/Reals/RiemannInt_SF.v | |
| parent | 05421cef04206a18cb30f6d115d27e7cb25ba0bf (diff) | |
Simplify some proofs.
This commit does not modify the signature of the involved modules, only
the opaque proof terms.
One has to wonder how proofs can bitrot so much that several occurrences
of "replace 4 with 4" start appearing.
Diffstat (limited to 'theories/Reals/RiemannInt_SF.v')
| -rw-r--r-- | theories/Reals/RiemannInt_SF.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 7885d697f..af7cbb940 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -83,11 +83,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)). |