proposition: Lemma E_trans_add_RV m : `E (X `+cst m) = `E X + m.
proof: Proof. rewrite /trans_add_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