Bloom filters debunked: Dispelling 30 Years of bad math with Coq Original article is at Bloom filters debunked: Dispelling 30 Years of bad math with Coq