diff options
| -rw-r--r-- | contrib/fourier/Fourier_util.v | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/contrib/fourier/Fourier_util.v b/contrib/fourier/Fourier_util.v index dcc45b66e4..e52597878c 100644 --- a/contrib/fourier/Fourier_util.v +++ b/contrib/fourier/Fourier_util.v @@ -136,14 +136,9 @@ replace 0 with (- -0). replace (- (n * / d)) with (- n * / d). replace (-0) with 0. red in |- *. -try exact H0. apply Ropp_gt_lt_contravar. -replace (- (n * / d)) with (- n * / d). -replace (-0) with 0. red in |- *. -try exact H0. -ring. -ring. +exact H0. ring. ring. ring. @@ -224,4 +219,4 @@ Qed. Lemma Rfourier_not_lt_ge : forall x y:R, (x < y -> False) -> x >= y. exact Rnot_lt_ge. -Qed.
\ No newline at end of file +Qed. |