proposition: Lemma prod_distr_rect : forall (A B : Type) (d1: Distr A) (d2:Distr B) (f:A->U)(g:B->U), mu (prod_distr d1 d2) (fun xy => f (fst xy) * g (snd xy)) == mu d1 f * mu d2 g.
proof: Proof. intros; unfold prod_distr; simpl. apply Oeq_trans with (mu d1 (fun x : A => mu d2 g * f x)). apply (mu_stable_eq d1). simpl; apply ford_eq_intro; intro x. rewrite (mu_stable_mult d2 (f x) g); auto. rewrite (mu_stable_mult d1 (mu d2 g) f); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)