We reason about measure equality by asserting axioms in Coq. The axioms constitute a small embedded monadic DSL, with standard primitives for random choice and scoring, and with intuitive equalities such as distributing random choices and multiplying scores. The axioms are only sound under the assumption that all functions are measurable and all measures are s-finite. Combined with inductive types and proofs, the axioms allow us to prove the correctness of probabilistic program transformations (including simplification and disintegration) and sampling techniques (including importance sampling and sequential Monte Carlo).