diff options
Diffstat (limited to 'theories/Reals/Sqrt_reg.v')
| -rw-r--r-- | theories/Reals/Sqrt_reg.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 10527442..d43baee8 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -339,7 +339,7 @@ Proof. rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5. - destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs. + destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs. unfold sqrt. rewrite Heqs. rewrite Rabs_R0; apply H2. rewrite Rabs_right. |