Formal probabilistic analysis using theorem proving