proposition: Lemma rsum_split: \sum_(x| x \in X) f0 x = \sum_(x| x \in S) f0 x + \sum_(x| x \in ~: S) f0 x.
proof: Proof. rewrite (bigID (fun x => x \in S)) /=; congr (_ + _). by apply eq_bigl => x /=; rewrite inE. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq natbin source_code