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/Ranalysis2.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/Ranalysis2.v')
| -rw-r--r-- | theories/Reals/Ranalysis2.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 27cb356a0..b749da0d2 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -423,10 +423,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. |