proposition: Lemma Var_scale k : `V (k `cst* X) = k ^ 2 * `V X.
proof: Proof. rewrite {1}/`V [in X in X = _]/= E_scalel_RV. pose Y : {RV P -> R} := k `cst* (X `+cst - `E X). rewrite (@E_comp_RV_ext _ P ((k `cst* X) `-cst k * `E X) Y) //; last first. rewrite boolp.funeqE => /= x. by rewrite /Y /scalel_RV /= /trans_min_RV /trans_add_RV; field. by rewrite E_comp_RV ?E_scalel_RV // => *; field. 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