From a6dc9774dbcf6ec553d69812b7f5422bede56585 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 29 Nov 2024 13:48:54 +0100 Subject: [PATCH] NIT --- theories/prob/distribution.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/prob/distribution.v b/theories/prob/distribution.v index a45e4fcb..28aee2c4 100644 --- a/theories/prob/distribution.v +++ b/theories/prob/distribution.v @@ -2449,6 +2449,7 @@ Ltac solve_distr := | |- (dmap _ _).(pmf) _ > 0 => apply dmap_pos; eexists; (split; [done|]); try done | |- (dunifP _).(pmf) _ > 0 => apply dunifP_pos + | |- (dunifv _ _).(pmf) _ > 0 => apply dunifv_pos end. Ltac solve_distr_mass := @@ -2458,6 +2459,7 @@ Ltac solve_distr_mass := | |- SeriesC (dmap _ _).(pmf) = 1 => rewrite dmap_mass // | |- SeriesC (dunif _).(pmf) = 1 => rewrite dunif_mass // | |- SeriesC (dunifP _).(pmf) = 1 => rewrite dunifP_mass // + | |- SeriesC (dunifv _ _).(pmf) = 1 => rewrite dunifv_mass // end . Ltac inv_dzero :=