Add lemma `le0_expectation_cdf` #1411

Job	Run time
rocq-core	1m 3s
coq	1m 5s
mathcomp-classical	2m 53s
mathcomp-analysis-single	14m 44s
mathcomp-reals	2m 14s
mathcomp-experimental-reals	3m 11s
mathcomp-analysis	12m 40s
mathcomp-reals-stdlib	3m 5s
ssprove	6m 2s
mathcomp-analysis-stdlib	1m 53s
mathcomp-infotheo	6m 59s
	55m 49s

Provide feedback