proposition: Lemma prod_distr_snd_eq : forall (A B : Type) (d1: Distr A) (d2:Distr B), mu d1 (fone A) == 1 -> im_distr (snd (A:=A) (B:=B)) (prod_distr d1 d2) == d2.
proof: Proof. intros; apply eq_distr_intro; intro g. rewrite im_distr_simpl. rewrite prod_distr_snd; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)