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