We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [Annals of Mathematics, 2002], and show that this analysis can be formalized in the bounded-arithmetic system VN C 1 (corresponding to the `` N C 1 reasoning''). As a corollary, we prove the assumption made by Jerabek [Annals of Pure and Applied Logic, 2011] that a construction of certain bipartite expander graphs can be formalized in VN C 1 . This in turn implies that every proof in Gentzen's sequent calculus LK of a monotone sequent can be simulated in the monotone version of LK (MLK) with only polynomial blowup in proof size, strengthening the quasipolynomial simulation result of Atserias, Galesi, and Pudlak [Journal of Computer and System Sciences, 2002].