proposition: Lemma __deprecated__dlet_dlet (mu : {distr T / R}) : \dlet_(x <- \dlet_(y <- mu) f1 y) f2 x =1 \dlet_(y <- mu) (\dlet_(x <- f1 y) f2 x).
proof: Proof. move=> z; unlock dlet => /=; rewrite /mlet /=. pose S y x := mu x * (f1 x y * f2 y z). rewrite (eq_psum (F2 := fun y => psum (S^~ y))) => [x|]. by rewrite -psumZ //; apply/eq_psum => y /=. rewrite __admitted__interchange_psum. + by move=> x; apply/summableZ/summable_mlet. + rewrite {}/S; apply/(le_summable (F2 := mu)) => //. move=> x; rewrite ge0_psum /= psumZ ?ler_piMr //. apply/(le_trans _ (le1_mu (f1 x)))/le_psum => //. by move=> y; rewrite mulr_ge0 //= ler_piMr ?le1_mu1. apply/eq_psum=> y /=; rewrite -psumZr //. by apply/eq_psum=> x /=; rewrite {}/S mulrA. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum