proposition: Lemma isd_mlet : isdistr mlet.
proof: Proof. split=> [x|J uqJ]; first by apply/ge0_psum. rewrite /mlet psum_bigop; first by move=> y x; rewrite mulr_ge0. move=> u; apply/(le_summable (F2 := mu)) => //. by move=> x; rewrite mulr_ge0 //= ler_piMr ?le1_mu1. apply/(le_trans _ (le1_mu mu))/le_psum => //. move=> x; rewrite sumr_ge0 /= => [y _|]; first by rewrite mulr_ge0. rewrite -mulr_sumr ler_piMr //; apply/(le_trans _ (le1_mu (f x))). have := summable_mu (f x) => /gerfinseq_psum => /(_ _ uqJ). by apply/(le_trans _)/ler_sum=> y _; apply/ler_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum