proposition: Lemma prod_distr_com_eq_compat : forall A B (d1: Distr A) (d2:Distr B) (f g: MF (A * B)), f == g -> prod_distr_com d1 d2 f -> prod_distr_com d1 d2 g.
proof: Proof. unfold prod_distr_com; intros; apply Oeq_trans with (mu (prod_distr d1 d2) f). apply mu_stable_eq; auto. apply Oeq_trans with (mu (prod_distr d2 d1) (arg_swap f)); auto. apply mu_stable_eq; unfold arg_swap,swap; simpl; apply ford_eq_intro; intro z. apply (ford_eq_elim H (snd z,fst z)). Qed.
imports: ALEA(Probas) ALEA(Utheory)