proposition: Lemma prod_dist_inde_rv : inde_rv X' Y'.
proof: Proof. apply/inde_rv_events => x y. rewrite (_ : [set _ | _ ] = finset (X @^-1 x) `*T); last first. by apply/setP => -[a b]; rewrite !inE. rewrite (_ : [set x | preim Y' (pred1 y) x] = T`* finset (Y @^-1 y)); last first. by apply/setP => -[a b]; rewrite !inE. by rewrite /P /inde_events -Pr_fdist_prod. 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