From da0fb740266cbc4934fcd3dcf40ae825ee6e5e54 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jul 2026 07:26:47 +0000 Subject: [PATCH] Fix psumZ rewrite direction for Rocq dev --- experimental_reals/distr.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v index 77b863797b..e69a345a76 100644 --- a/experimental_reals/distr.v +++ b/experimental_reals/distr.v @@ -965,7 +965,7 @@ rewrite interchange_psum /=; last first. apply/eq_psum=> y /=; rewrite mulrC -psumZ //. by apply/eq_psum=> x /=; rewrite mulrCA. + have := summable_pr E (dlet f mu); apply/eq_summable. - by move=> x; rewrite dletE psumZ ?ler0n. + by move=> x; rewrite dletE -psumZ ?ler0n. + by move=> y; apply/summable_condl/summable_mlet. Qed.