proposition: Lemma prod_distr_com_cte : forall (A B : Type) (d1: Distr A) (d2:Distr B) (c:U), prod_distr_com d1 d2 (fcte (A*B) c).
proof: Proof. intros; apply prod_distr_com_eq_compat with (fun z => fcte A c (fst z) * fone B (snd z)). simpl; auto. apply prod_distr_com_rect. Qed.
imports: ALEA(Probas) ALEA(Utheory)