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/Rpower.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/Rpower.v')
| -rw-r--r-- | theories/Reals/Rpower.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index f62ed2a6c..b8040bb4f 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -456,7 +456,7 @@ Proof. unfold Rpower; auto. rewrite Rpower_mult. rewrite Rinv_l. - replace 1 with (INR 1); auto. + change 1 with (INR 1). repeat rewrite Rpower_pow; simpl. pattern x at 1; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)). ring. |