Library Coq.micromega.Fourier
Require
Import
Lra
.
Require
Export
Fourier_util
.
#[
deprecated
(
since
= "8.9.0",
note
= "Use lra instead.")]
Ltac
fourier
:=
lra
.