diff options
| author | thery | 2019-03-28 15:19:09 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-05-07 14:18:24 +0000 |
| commit | 94f3caa81cf2f681b66da9f3f69a9d8b881303e1 (patch) | |
| tree | f9a66df72f8fbcd3397acab7ea5627988046a3c1 /theories | |
| parent | e30d52a3c724a71bf43b46416c09e4b6ef1d1f67 (diff) | |
Improve field_simplify on fractions with constant denominator
Before this patch, `x` was "simplified" to `x / 1`.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Reals/Ratan.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index 03e6ff61ab..38bed570a3 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -324,8 +324,6 @@ unfold cos_approx; simpl; unfold cos_term. rewrite !INR_IZR_INZ. simpl. field_simplify. -unfold Rdiv. -rewrite Rmult_0_l. apply Rdiv_lt_0_compat ; now apply IZR_lt. Qed. @@ -1612,4 +1610,3 @@ Lemma PI_ineq : Proof. intros; rewrite <- Alt_PI_eq; apply Alt_PI_ineq. Qed. - |