Proof of Weierstrass' theorem formalised in Rocq, using Bernstein polynomials, following lectures notes of Nicolas Brisebarre. Author: Damien Pous, 2025 Licence: GPL3.0