proposition: Lemma bipart_dominates : let A_ := fun b => if b then [set a | (P a < Q a)%mcR] else [set a | (Q a <= P a)%mcR] in forall (cov : A_ 0 :|: A_ 1 = [set: A]) (dis : A_ 0 :&: A_ 1 = set0), bipart dis cov P `<< bipart dis cov Q.
proof: Proof. move=> A_ cov dis; apply/dominatesP => /= b. rewrite !ffunE => /psumr_eq0P H. transitivity (\sum_(a | a \in A_ b) 0%R). apply eq_bigr => // a ?. by rewrite (dominatesE P_dom_by_Q) // H // => a' ?; exact/pos_ff_ge0. by rewrite big_const iter_addR mulR0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext logb ln_facts bigop_ext convex fdist divergence variation_dist partition_inequality