coq_fft_proof Proof that the FFT implements the DFT, written in Coq. This proof was developed using Coq 8.10.1. Usage Compile the complex numbers library with: coqc Complex.v Then you can proceed to load the FFT.v into CoqIDE and step through it.
