diff options
Diffstat (limited to 'theories/Reals/ArithProp.v')
| -rw-r--r-- | theories/Reals/ArithProp.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 6fca9c8ad..7d9fff276 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -106,7 +106,7 @@ Proof. split. ring. unfold k0; case (Rcase_abs y) as [Hlt|Hge]. - assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl; + assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; change (IZR 1) with 1; unfold Rminus. replace (- ((1 + - IZR (up (x / - y))) * y)) with ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ]. @@ -140,7 +140,7 @@ Proof. rewrite <- Ropp_mult_distr_r_reverse; rewrite (Ropp_inv_permute _ H); elim H0; unfold Rdiv; intros H1 _; exact H1. apply Ropp_neq_0_compat; assumption. - assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; simpl; + assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; change (IZR 1) with 1; cut (0 < y). intro; unfold Rminus; replace (- ((IZR (up (x / y)) + -1) * y)) with ((1 - IZR (up (x / y))) * y); |