Reasoning about conditional probabilities in a higher-order-logic theorem prover