proposition: Lemma E_trans_min_RV m : `E (X `-cst m) = `E X - m.
proof: Proof. rewrite /trans_min_RV /=. transitivity (\sum_(u in U) (X u * P u + - m * P u)). by apply eq_bigr => u _ /=; rewrite mulRDl. by rewrite big_split /= -big_distrr /= FDist.f1 mulR1. 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