proposition: Lemma V_sum_2 : X \= X1 @+ X2 -> P |= X1' _|_ X2' -> `V X = `V X1 + `V X2.
proof: Proof. move=> H ?; rewrite !VarE E_id_rem // (E_sum_2 H) sqrRD. by rewrite /Ex /= -/P1 -/P2; 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