diff options
| author | Michael Soegtrop | 2019-05-10 13:58:31 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2019-05-10 13:58:31 +0200 |
| commit | 73f921f9634b9ccb587b2f85869d88eb12983d0f (patch) | |
| tree | d8e17412e42f9085fbaf000484f83ea98c6e65ea /theories | |
| parent | c659b96eaa7bb5e401786546bb293a31e5f3c3d4 (diff) | |
| parent | 281e6657c7fe5033a13c7a2fd2b6cc6f51cb6911 (diff) | |
Merge PR #9854: Improve field_simplify on fractions with constant denominator
Reviewed-by: MSoegtropIMC
Ack-by: Zimmi48
Reviewed-by: amahboubi
Reviewed-by: vbgl
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. - |