Kangfeng Ye, Simon Foster, Jim Woodcock: Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving. RAMiCS 2021: 465-482