General Probability in Coq

We have developed a general probability library in the Coq proof assistant intended for applications in machine learning and stochastic approximation. We will discuss design decisions and lessons learned.