Formalization of the Standard Uniform random variable