proposition: Lemma prod_distr_com_mult : forall (A B : Type) (d1: Distr A) (d2:Distr B) (k:U)(f:MF (A*B)), prod_distr_com d1 d2 f -> prod_distr_com d1 d2 (fmult k f).
proof: Proof. unfold prod_distr_com; intros. rewrite (mu_stable_mult (prod_distr d1 d2) k f). rewrite H. rewrite <- (mu_stable_mult (prod_distr d2 d1) k (arg_swap f)); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)