diff options
Diffstat (limited to 'theories/Reals/R_sqrt.v')
| -rw-r--r-- | theories/Reals/R_sqrt.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 5c975c3f5..0c1e0b7e8 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -420,10 +420,10 @@ Proof. rewrite (Rmult_comm (/ a)). rewrite Rmult_assoc. rewrite <- Rinv_mult_distr. - replace (2 * (2 * a) * a) with (Rsqr (2 * a)). + replace (4 * a * a) with (Rsqr (2 * a)). reflexivity. ring_Rsqr. - rewrite <- Rmult_assoc; apply prod_neq_R0; + apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ]. apply (cond_nonzero a). assumption. |