proposition: Lemma prod_distr_snd : forall (A B : Type) (d1: Distr A) (d2:Distr B) (g:B->U), mu (prod_distr d1 d2) (fun xy => g (snd xy)) == mu d1 (fone A) * mu d2 g.
proof: Proof. intros; rewrite <- prod_distr_rect. apply (mu_stable_eq (prod_distr d1 d2)). simpl; apply ford_eq_intro; unfold UP.fone; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)