proposition: Lemma prod_distr_com_rect : forall (A B : Type) (d1: Distr A) (d2:Distr B) (f:A->U)(g:B->U), prod_distr_com d1 d2 (fun xy => f (fst xy) * g (snd xy)).
proof: Proof. red; intros. rewrite prod_distr_rect. apply Oeq_trans with (mu (prod_distr d2 d1) (fun yx => g (fst yx) * f (snd yx))). rewrite prod_distr_rect; auto. apply mu_stable_eq; simpl; apply ford_eq_intro; intro yx; unfold arg_swap; simpl; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)