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/SeqProp.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/SeqProp.v')
| -rw-r--r-- | theories/Reals/SeqProp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 5a2a07c42..3697999f7 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -1167,7 +1167,7 @@ Proof. assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros. rewrite H4 in H7; rewrite <- INR_IZR_INZ in H7. simpl in H7; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H2 H7)). - replace 1 with (INR 1); [ apply le_INR | reflexivity ]; apply le_n_S; + apply (le_INR 1); apply le_n_S; apply le_O_n. apply le_IZR; simpl; left; apply Rlt_trans with (Rabs x). assumption. |