In multiple domains, large amounts of data are generated daily and combined to be analyzed. The interpretation of these analyses requires tracking the provenance of the combined data with respect to the initial, raw data. The correctness of the provenance is crucial in many critical domains, such as in medicine to prescribe treatments. In this article, we propose the first provenance-aware extended relational algebra formalized in a proof assistant (Coq), for a non trivial subset of database queries: queries containing aggregates, null values, and correlated sub-queries. The formalization is validated by an adequacy proof with respect to standard evaluation of queries. This development is a first step towards a posteriori certification of provenance for data manipulation, with strong guaranties.