proposition: Lemma Prod_dominates_Joint : P `<< P`1 `x P`2.
proof: Proof. apply/dominatesP => -[a b]. rewrite fdist_prodE /= => /eqP. rewrite mulf_eq0 => /orP -[/eqP P1a| /eqP P2b]; by [rewrite dom_by_fdist_fst | rewrite dom_by_fdist_snd]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext