diff options
Diffstat (limited to 'theories/Reals/Rbasic_fun.v')
| -rw-r--r-- | theories/Reals/Rbasic_fun.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index c889d7347..fe5402e6e 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -613,11 +613,12 @@ Qed. Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Z.abs z). Proof. - intros z; case z; simpl; auto with real. - apply Rabs_right; auto with real. - intros p0; apply Rabs_right; auto with real zarith. + intros z; case z; unfold Zabs. + apply Rabs_R0. + now intros p0; apply Rabs_pos_eq, (IZR_le 0). + unfold IZR at 1. intros p0; rewrite Rabs_Ropp. - apply Rabs_right; auto with real zarith. + now apply Rabs_pos_eq, (IZR_le 0). Qed. Lemma abs_IZR : forall z, IZR (Z.abs z) = Rabs (IZR z). |