proposition: Lemma Ex_ge0 : (forall u, 0 <= X u) -> 0 <= Ex.
proof: Proof. move=> H; apply/RleP/sumr_ge0 => u _; rewrite mulr_ge0//; exact/RleP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist