proposition: Lemma prod_distr_com_refl : forall A B (d1:distr A) (d2:distr B) (f:MF (A*B)), prod_distr_com d1 d2 f -> prod_distr_com d2 d1 (arg_swap f).
proof: Proof. red; intros. apply Oeq_sym; apply Oeq_trans with (mu (prod_distr d1 d2) f); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)