proposition: Lemma prod_distr_com_plus : forall (A B : Type) (d1: Distr A) (d2:Distr B) (f g:MF (A*B)), fplusok f g -> prod_distr_com d1 d2 f -> prod_distr_com d1 d2 g -> prod_distr_com d1 d2 (fplus f g).
proof: Proof. unfold prod_distr_com; intros. rewrite (mu_stable_plus (prod_distr d1 d2) (f:=f) (g:=g) H). rewrite H0; rewrite H1. rewrite <- (mu_stable_plus (prod_distr d2 d1) (f:=arg_swap f) (g:=arg_swap g)); auto. red; unfold arg_swap,swap,finv; simpl; intro z; apply (H (snd z,fst z)). Qed.
imports: ALEA(Probas) ALEA(Utheory)