diff options
| -rw-r--r-- | contrib7/fourier/Fourier_util.v | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/contrib7/fourier/Fourier_util.v b/contrib7/fourier/Fourier_util.v index 0f36eda8cb..37a93dcd3d 100644 --- a/contrib7/fourier/Fourier_util.v +++ b/contrib7/fourier/Fourier_util.v @@ -149,14 +149,9 @@ Replace R0 with (Ropp (Ropp R0)). Replace (Ropp (Rmult n (Rinv d))) with (Rmult (Ropp n) (Rinv d)). Replace (Ropp R0) with R0. Red. -Try Exact H0. Apply Rgt_Ropp. -Replace (Ropp (Rmult n (Rinv d))) with (Rmult (Ropp n) (Rinv d)). -Replace (Ropp R0) with R0. Red. -Try Exact H0. -Ring. -Ring. +Exact H0. Ring. Ring. Ring. |