https://github.com/math-comp/analysis/blob/87151818a5463096620262f95bd35daaec0a9661/theories/probability.v#L77 the notation should better be at level 5 with P and X at level 4 @hoheinzollern @t6s