proposition: Lemma E_sub_RV : `E (X `- Y) = `E X - `E Y.
proof: Proof. rewrite {3}/Ex -addR_opp big_morph_oppR -big_split /=. apply eq_bigr => u _; by rewrite -mulNR -mulRDl. 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