Probabilistic programs with sampling and scoring are used to write probabilistic models to make probabilistic inferences. Despite their effectful nature, such programs can actually be verified by means of equational reasoning. We propose a formal foundation in the Rocq prover to mechanize such verifications. For that purpose, we extend an existing library for Lebesgue integration and formalize standard probability distributions. Using the resulting library, we extend the intrinsically-typed syntax and the kernel-based semantics of an encoding of a probabilistic programming language. Thanks to these extensions, we mechanize the main running examples of Shan’s tutorial on equational reasoning for probabilistic programming at POPL 2018’s TutorialFest.