proposition: Lemma im_distr_comp : forall A B C (f:A->B) (g:B->C) (m:Distr A), im_distr g (im_distr f m) == im_distr (fun a => g (f a)) m.
proof: Proof. intros; apply eq_distr_intro; simpl; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)