proposition: Lemma prod_distr_com_inv : forall (A B : Type) (d1: Distr A) (d2:Distr B) (f:MF (A*B)), prod_distr_com d1 d2 f -> prod_distr_com d1 d2 (finv f).
proof: Proof. unfold prod_distr_com; intros. rewrite (mu_inv_minus (prod_distr d1 d2) f). rewrite H. assert (H1:=prod_distr_com_one d1 d2); red in H1. rewrite H1. rewrite <- (mu_inv_minus (prod_distr d2 d1) (arg_swap f)); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)