Formally Analyzing Expected Time Complexity of Algorithms Using Theorem Proving