Library Coq.fourier.Fourier

Require Export Field.
Require Export DiscrR.
Require Export Fourier_util.

Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR).

Ltac fourier_eq := apply Rge_antisym; fourier.