1 2 3 4 5
Require Import Lra. Require Export Fourier_util. #[deprecated(since = "8.9.0", note = "Use lra instead.")] Ltac fourier := lra.