proposition: Lemma prod_distr_com_lub : forall (A B : Type) (d1: Distr A) (d2:Distr B) (f:natO-m>MF (A*B)), (forall n, prod_distr_com d1 d2 (f n)) -> prod_distr_com d1 d2 (lub f).
proof: Proof. unfold prod_distr_com; intros. rewrite (lub_comp_eq f (mu_continuous (prod_distr d1 d2))). apply Oeq_trans with (lub (mu (prod_distr d2 d1) @ (Arg_swap A B @ f))). apply lub_eq_compat; apply fmon_eq_intro; intro n. repeat rewrite fmon_comp_simpl. rewrite H; auto. rewrite <- lub_comp_eq; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)