diff options
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. |