diff --git a/doc/tactics/rnd.rst b/doc/tactics/rnd.rst
index 1284cc07b5..28e74f9715 100644
--- a/doc/tactics/rnd.rst
+++ b/doc/tactics/rnd.rst
@@ -121,6 +121,15 @@ If the conclusion is a probabilistic Hoare logic statement judgement whose progr
     which can be provided explicitly. When `E`` is not
     specified, it is inferred from the current postcondition.
 
+    The upper bound is checked in the (partial-correctness) postcondition,
+    which only constrains the terminating runs of the program preceding the
+    sampling. The non-terminating runs contribute probability 0, so the
+    tactic additionally requires the bound to be non-negative, as a separate
+    goal quantified over all memories (a probabilistic Hoare logic judgement
+    whose bound is negative in some memory is false, whether or not that
+    memory satisfies the precondition). That goal is closed automatically
+    when it is trivial.
+
 .. ecproof::
    :title: Probabilistic Hoare logic example (upper bound)
 
@@ -145,9 +154,11 @@ If the conclusion is a probabilistic Hoare logic statement judgement whose progr
         (* The post now has two clauses, the first is to prove the
            probability upper bound on the event, and the second one is to
            prove that the event holding implies the
-           previous postcondition. *)
-     skip => *;split.
-     + by smt(dbool1E). 
+           previous postcondition. A second goal requires the bound to
+           be non-negative. *)
+     + skip => *;split.
+       + by smt(dbool1E).
+       by smt().
      by smt().
    qed.
 
diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec
index 0f06dec806..ece92fab5a 100644
--- a/examples/ChaChaPoly/chacha_poly.ec
+++ b/examples/ChaChaPoly/chacha_poly.ec
@@ -2238,8 +2238,9 @@ section PROOFS.
       rcondf 1; 1: by auto; smt(size_eq0 size_ge0).
       by hoare; auto; smt(size_ge0 ge0_pr_zeropol).
     call(: Mem.lc = l /\ ROout.m = roout /\ 0 < size l <= qdec /\ 0 < size l1 ==> UF.forged); auto.
-    bypr=> {&m} &m [#] *.
-
+    bypr=> {&m} &m. 
+    split => [|[#] *].
+    - smt(ge0_pr_zeropol size_ge0).
     fel 4 UFCMA4.cforged                (* the query counter *)
         (fun i => (size (filter (fun (c:ciphertext) => c.`1 = nth witness l1 i) l))%r * pr_zeropol)
                                         (* the probability of bad occuring during ith query *)
@@ -2254,7 +2255,8 @@ section PROOFS.
     + auto=> /> /#.
     + proc; sp 2.
       if; last by hoare; auto; smt(size_ge0 ge0_pr_zeropol).
-      inline*; wp; rnd; auto=> &h /> *.
+      inline*; wp; rnd; last by move=> &h />; smt(size_ge0 ge0_pr_zeropol).
+      auto=> &h /> *.
       by apply pr_TPI_ok_filter=> //=.
     + by move=> c; proc; sp; inline*; sp; if; auto=> /#.
     + by move=> b c; proc; inline*; sp; rcondf 1; auto. 
@@ -2270,8 +2272,9 @@ section PROOFS.
     + inline*; sp; rcondf 1; 1: by auto=> &h />; smt(size_ge0 size_eq0).
       by hoare; auto; smt(size_ge0 mu_bounded).
     call(: Mem.lc = l /\ ROout.m = roout /\ 0 < size l <= qdec /\ 0 < size l2 ==> UFCMA.bad2); auto.
-    bypr=> {&m} &m [#] *.
-
+    bypr=> {&m} &m.
+    split => [| [#] *]. search (0%r <= _ * _).
+    + apply mulr_ge0; smt(size_ge0 ge0_mu).
     fel 4 UFCMA.cbad2                   (* the query counter *)
         (fun i => (size (filter (fun (c:ciphertext) => c.`1 = nth witness l2 i) l))%r * pr1_poly_out)
                                         (* the probability of bad occuring during ith query *)
@@ -2285,12 +2288,14 @@ section PROOFS.
     + by move=> />.
     + by auto=> /> /#.
     + proc; inline*; sp 2; if; 2: auto=> />.
-      wp; rnd=> />; sp; conseq(:_==> true); 2: by auto. 
+      wp; rnd; last by move=> &h />; smt(size_ge0 ge0_mu1).
+      move=> />; sp; conseq(:_==> true); 2: by auto.
       move=> &h /> *. 
       pose lc := List.map _ _.
       have h := mu_mem_le_mu1 dpoly_out lc pr1_poly_out _; 1: smt(dpoly_out_funi).
       rewrite (StdOrder.RealOrder.ler_trans _ _ _ h) //=  ler_wpmul2r; 1: smt(mu_bounded).
       by rewrite le_fromint IntOrder.lerr_eq //= size_map.
+    + move => &hr; smt(size_ge0 ge0_mu mulr_ge0).
     + move=> c; proc; inline*; sp; rcondt 1; 1: auto=> />.
       by wp -1=> />; conseq(:_==> true); auto; smt().
     + by move=> b c; proc; inline*; sp; rcondf 1; auto=> />.
@@ -2508,7 +2513,7 @@ section PROOFS.
   swap 3 1; swap [4..6] 12; wp -10 -10=> /=.
   swap 4 4; wp -1 -1.
   conseq(:_==> ={c1, t0, RO.m, Mem.log, Mem.lc}); [2:sim=> /> /#].
-  move=> /> &1 &2 *; do ! split => />.
+  move=> /> &1 &2 H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H15 *; do ! split => />.
   - smt().  
   - smt().  
   - rewrite size_cat !size_map make_lbad1_size_cons3 //= /#.
@@ -2517,12 +2522,17 @@ section PROOFS.
     smt(get_setE).
   - move => n; case: (n = n{!2}) => />; first by rewrite /dom get_setE.
     smt(get_setE).
-  - move=> ? ? H15; have:=H15; rewrite mem_cat=> [#][] H16 *.
+  - move=> ? ? H16; have:=H16; rewrite mem_cat=> [#][] H17 *.
     + smt(get_setE).
-    have:= H16; rewrite mapP /= => [#][] t2 [#] h <<- <<-; have:=h.
+    have:= H17; rewrite mapP /= => [#][] t2 [#] h <<- <<-; have:=h.
     rewrite mapP /==> [#] [][] x1 x2 x3 x4 /=; rewrite mem_filter /= => [#] <<- ? ->>.
     smt(get_setE).
-  smt(List.mem_filter mem_cat mapP).
+  move => [/H10 [][] tt ? [] t_mem /= <<-|
+           H16 /mapP [] ct [] /List.mem_filter [] /= <<- H17 ->>].
+  - smt(List.mem_filter mem_cat mapP). 
+  exists (ct.`4, ct.`4) => /=.
+  rewrite mem_cat.
+  smt(mapP List.mem_filter).
   qed.
 
   local clone EventPartitioning as EP with 
@@ -2731,7 +2741,8 @@ section PROOFS.
   + by rewrite /= BRA.big_int1 /=. 
   + by auto=> />.
   + proc. 
-    rcondt 2; 1: auto; wp=> />; rnd=> />; skip=> /> &hr *.
+    rcondt 2; 1: auto; wp=> />; rnd; last by move=> &hr />; smt(ge0_mu1).
+    move=> />; skip=> /> &hr *.
     by have <- //=:=dpoly_out_funi witness ti{hr}.
   + move=> c; proc; auto=> />; smt().
   by move=> b c; proc; auto.
diff --git a/examples/PIR.ec b/examples/PIR.ec
index 41317f0e71..3a3caf077c 100644
--- a/examples/PIR.ec
+++ b/examples/PIR.ec
@@ -196,13 +196,16 @@ lemma Pr_PIR_s i0 &m x :
 proof.
   byphoare=> // {i0};proc;inline *;wp.
   case: (is_restr x N);first last.
-  + conseq (_ : _ ==> _ : = 0%r) => [ _ -> // | ].
+  + conseq (_ : _ ==> _ : = 0%r) => [ _ | ].
+    + smt(expr_ge0 divr_ge0).
     hoare;conseq (_ : _ ==> is_restr (oflist PIR.s) N); 1:by smt().
     while (0<= j <= N /\ is_restr (oflist PIR.s) j).
     + by auto => &m1 />;rewrite oflist_cons;smt (is_restrS is_restr_addS).
     auto=> ?;rewrite -set0E;smt (is_restr_fset0 N_pos).
   sp; conseq (_ : _ ==> _ : = (if (oflist PIR.s) = restr x j then 1%r/2%r^(N-j) else 0%r)).
   + move=> {&m} &m />;rewrite -set0E.
+    split.
+    + smt(expr_ge0 invr_ge0).
     have -> // : fset0 = restr x 0.
     + by apply fsetP=> z;rewrite /restr !inE mem_oflist mem_iota /#.
   conseq (_ : _ ==> oflist PIR.s = restr x j) (_: _ ==> j = N) => //;1:smt().
@@ -222,7 +225,8 @@ proof.
         by conseq H=> /#.
       + by hoare;auto.
       smt().
-    conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
+    conseq (_ : _ : = (1%r / 2%r ^ (N - j))).
+    + smt(divr_ge0 expr_ge0).
     exists * j, PIR.s;elim * => j0 s0.
     seq 3: (b = j0 \in x) (1%r/2%r) (1%r / 2%r ^ (N - (j0+1))) _ 0%r
         (1 <= j <= N /\ j = j0 + 1 /\ (PIR.s = if b then j0 :: s0 else s0) /\
@@ -230,7 +234,9 @@ proof.
     + by auto => /> /#.
     + by wp => /=;rnd (pred1 (j0 \in x));skip => /> &hr;rewrite dbool1E.
     + conseq H=> />.
-      + case: (j0 \in x) => Hjx ?? His Hof.
+      + split.
+        + smt(divr_ge0 expr_ge0).
+        case: (j0 \in x) => Hjx ?? His Hof.
         + by rewrite oflist_cons restrS 1:/# Hjx Hof.
         by rewrite restrS 1:/# Hjx Hof /= fset0U.
       smt (is_restrS is_restr_addS oflist_cons).
@@ -250,15 +256,17 @@ lemma Pr_PIR_s' i0 &m x :
 proof.
   byphoare=> // {i0};proc;inline *;wp.
   case: (is_restr x N);first last.
-  + conseq (_ : _ ==> _ : = 0%r) => [ _ -> // | ].
+  + conseq (_ : _ ==> _ : = 0%r).
+    + smt(divr_ge0 expr_ge0).
     hoare;conseq (_ : _ ==> is_restr (oflist PIR.s') N); 1:by smt().
     while (0<= j <= N /\ is_restr (oflist PIR.s') j).
     + auto;smt (oflist_cons is_restrS is_restr_addS).
     auto=> ?;rewrite -set0E;smt (is_restr_fset0 N_pos).
   sp; conseq (_ : _ ==> _ : = (if (oflist PIR.s') = restr x j then 1%r/2%r^(N-j) else 0%r)).
   + move=> {&m} &m />;rewrite -set0E.
-    have -> // : fset0 = restr x 0.
+    have ->: fset0 = restr x 0.
     + by apply fsetP=> z;rewrite /restr !inE mem_oflist mem_iota /#.
+    smt(invr_ge0 expr_ge0).
   conseq (_ : _ ==> oflist PIR.s' = restr x j) (_: _ ==> j = N) => //;1:smt().
   + while(0 <= j <= N);auto;smt (N_pos).
   conseq (: (0 <= j <= N /\ is_restr (oflist PIR.s') j) ==> _).
@@ -276,7 +284,8 @@ proof.
         by conseq H => /#.
       + by hoare; auto.
       smt().
-    conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
+    conseq (_ : _ : = (1%r / 2%r ^ (N - j))).
+    + smt(divr_ge0 expr_ge0).
     exists * j, PIR.s';elim * => j0 s0.
     seq 3: (b = ((j0 = i) ^^ (j0 \in x))) (1%r/2%r) (1%r / 2%r ^ (N - (j0+1))) _ 0%r
         (1 <= j <= N /\ j = j0 + 1 /\ (PIR.s' = if (j0=i) then (if b then s0 else j0::s0) else if b then j0 :: s0 else s0) /\
@@ -284,7 +293,10 @@ proof.
     + by auto => /#.
     + by wp => /=;rnd (pred1 ((j0 = i) ^^ (j0 \in x)));skip => /> &hr;rewrite dbool1E.
     + conseq H => />.
-      + move=> &hr ?? His Hof;case: (j0 = i{hr}) => /=.
+      + move=> &hr. 
+        split. 
+        + smt(invr_ge0 expr_ge0).
+        move => ?? His Hof;case: (j0 = i{hr}) => /=.
         + rewrite xorC xor_true => <<-.
           case: (j0 \in x) => Hjx.
           + by rewrite restrS 1:/# Hjx /= oflist_cons Hof.
diff --git a/examples/PRG.ec b/examples/PRG.ec
index d65a0153fb..c50faf5e19 100644
--- a/examples/PRG.ec
+++ b/examples/PRG.ec
@@ -512,6 +512,8 @@ section.
   conseq (_ : _ : <= (if Bad P.logP F.m then 1%r else
       (sumid (qF + size P.logP) (qF + n))%r / Support.card%r)).
   + move=> /> &hr.
+    split.
+    + smt(Support.card_gt0 ge0_qP ge0_qF).
     have /= -> /= szlog_le_qP szm_le_qF := negBadE A AaL [] F.m{hr}.
     apply/ler_wpmul2r; first smt w=Support.card_gt0. apply/le_fromint.
     rewrite -{1}(@add0z qF) big_addn /= /predT -/predT.
@@ -524,18 +526,27 @@ section.
   while (n <= qP /\ card (fdom F.m) <= qF).
   + move=> Hw; exists* P.logP, F.m; elim* => logPw m.
     case: (Bad P.logP F.m).
-    + by conseq (_ : _ : <= (1%r))=> // /#.
+    + conseq (_ : _ : <= (1%r))=> //= &hr.
+      split => [|/#].
+      case (Bad P.logP{hr} F.m{hr}) => //=.
+      apply divr_ge0; 2: smt(Support.card_gt0).
+      apply/le_fromint/sumr_ge0_seq.
+      smt(mem_range size_ge0 ge0_qF).
     seq 2: (Bad P.logP F.m)
            ((qF + size logPw)%r / Support.card%r) 1%r 1%r
            ((sumid (qF + (size logPw + 1)) (qF + n))%r / Support.card%r)
            (F.m = m /\ r::logPw = P.logP /\
             n <= qP /\ card (fdom F.m) <= qF)=> //.
     + by wp; rnd=> //.
-    + wp; rnd; auto=> /> &0 _ /le_fromint domF_le_qF _ /pr_newbad ->.
+    + wp; rnd; last by move=> &hr />; smt(Support.card_gt0 size_ge0 ge0_qF).
+      auto=> /> &0 _ /le_fromint domF_le_qF _ /pr_newbad ->.
       apply: ler_wpmul2r.
       + by apply: invr_ge0; smt(Support.card_gt0).
       by rewrite !fromintD ler_add2r.
     + conseq Hw; progress=> //.
+      + apply divr_ge0; 2: smt(Support.card_gt0).
+        apply/le_fromint/sumr_ge0_seq.
+        smt(mem_range size_ge0 ge0_qF).
       by rewrite H1 /= (Ring.IntID.addrC 1) lerr.
     progress=> //; rewrite H2 /= -mulrDl addrA -fromintD.
     rewrite
diff --git a/examples/Upto.ec b/examples/Upto.ec
index 9fb77e06e7..7fc79c8744 100644
--- a/examples/Upto.ec
+++ b/examples/Upto.ec
@@ -132,7 +132,7 @@ fel 2 Experiment.WO.cO g qO (Experiment.WO.bad)
   + by hoare; auto=> /#.
   swap 1 1; wp.
   exists* Experiment.WO.cO; elim* => cO.
-  conseq (: _ : (g cO))=> //.
+  conseq (: _ : (g cO))=> //; 1:smt().
   exists* Experiment.WO.bad; elim* => b.
   call (hbound_bad cO); auto; smt().
 + move=> c; proc; sp; if=> //; wp.
diff --git a/examples/cramer-shoup/cramer_shoup.ec b/examples/cramer-shoup/cramer_shoup.ec
index b66255ee1d..3415123e30 100644
--- a/examples/cramer-shoup/cramer_shoup.ec
+++ b/examples/cramer-shoup/cramer_shoup.ec
@@ -614,7 +614,8 @@ section Security_Aux.
 
   local lemma pr_G2_res &m: Pr[G2.main() @ &m : res] <= 1%r/2%r.
   proof.
-    byphoare=> //;proc;rnd;conseq (_: _ ==> true) => //=.
+    byphoare=> //;proc;rnd; last by move=> &hr /=; smt().
+    conseq (_: _ ==> true) => //=.
     by move=> ?;rewrite DBool.dbool1E.
   qed.
 
@@ -761,7 +762,7 @@ section Security_Aux.
   local lemma pr_G3_y2log &m :
     Pr[G3.main() @ &m : G1.y2 \in G3.y2log] <= PKE_.qD%r / order%r.
   proof.
-    byphoare => //;proc;wp;rnd.
+    byphoare => //;proc;wp;rnd; last by move=> &hr /=; smt(qD_pos gt1_q).
     conseq (_: _ ==> size G3.y2log <=  PKE_.qD) => /=.
     + move=> y2log Hsize;apply (ler_trans ((size y2log)%r/order%r)).
       + by apply (mu_mem_le_mu1 dt y2log (inv order%r)) => x;rewrite dt1E.
@@ -906,7 +907,8 @@ section Security_Aux.
     + hoare;conseq (_ : _ ==> true) => // /#.
     + move=> &hr _;apply lerr_eq;ring.
     + by auto.
-    + rnd;skip => /> &hr Hsize _;pose m' := map _ _.
+    + rnd; last by move=> &hr /=; smt(qD_pos gt1_q).
+      skip => /> &hr Hsize _;pose m' := map _ _.
       apply (mu_mem_le_mu1_size dt m') => //.
       + by rewrite /m' size_map.
       by move=> ?;rewrite dt1E.
@@ -916,7 +918,8 @@ section Security_Aux.
     + hoare;conseq (_ : _ ==> true) => // /#.
     + move=> &hr _;apply lerr_eq;ring.
     + by auto.
-    + rnd;skip => /> &hr Hsize _;pose m' := map _ _.
+    + rnd; last by move=> &hr /=; smt(qD_pos gt1_q).
+      skip => /> &hr Hsize _;pose m' := map _ _.
       apply (mu_mem_le_mu1_size (dt \ pred1 G1.u{hr}) m') => //.
       + by rewrite /m' size_map.
       move=> x;rewrite dexcepted1E {1}/pred1.
@@ -932,12 +935,14 @@ section Security_Aux.
       + rewrite expr2; smt (gt1_q).
       + smt (gt1_q).
     + by auto.
-    + rnd;skip => /> &hr Hsize _;pose m' := map _ _.
+    + rnd; last by move=> &hr /=; smt(qD_pos gt1_q).
+      skip => /> &hr Hsize _;pose m' := map _ _.
       apply (mu_mem_le_mu1_size dt m') => //.
       + by rewrite /m' size_map.
       by move=> ?;rewrite dt1E.
     conseq (_ : _ ==> (r \in map (fun (g4 : ciphertext) => loge g4.`4) G3.cilog)) => //.
-    rnd;skip => /> &hr Hsize _;pose m' := map _ _.
+    rnd; last by move=> &hr /=; smt(qD_pos gt1_q).
+    skip => /> &hr Hsize _;pose m' := map _ _.
     apply (mu_mem_le_mu1_size dt m') => //.
     + by rewrite /m' size_map.
     by move=> ?;rewrite dt1E.
diff --git a/examples/global-hybrid/GlobalHybridExamp1.ec b/examples/global-hybrid/GlobalHybridExamp1.ec
index 4c70d40937..770faa002f 100644
--- a/examples/global-hybrid/GlobalHybridExamp1.ec
+++ b/examples/global-hybrid/GlobalHybridExamp1.ec
@@ -188,7 +188,7 @@ seq 3 :
   (1%r - (1%r / (2 ^ n)%r))
   0%r.
 + by auto.
-+ by wp; rnd (pred1 def); auto; smt(mu1_dt).
++ by wp; rnd (pred1 def); auto; smt(mu1_dt StdOrder.IntOrder.expr_gt0).
 + conseq (: _ ==> _ : = 1%r).
   while (true) (m - i) => [z |].
   + by auto; smt(dt_ll).
diff --git a/examples/plug-and-pray/Plug_and_Pray.eca b/examples/plug-and-pray/Plug_and_Pray.eca
index 187f9ae29d..7cc43d7b4a 100644
--- a/examples/plug-and-pray/Plug_and_Pray.eca
+++ b/examples/plug-and-pray/Plug_and_Pray.eca
@@ -49,7 +49,8 @@ seq  1: (phi (glob G) o)
         _ 0%r => //.
   (* FIXME: This is more verbose than it should be! *)
 + call (: (glob G) = (glob G){m} /\ x = x0 ==> phi (glob G) res) => //.
-  bypr=> &m0 @/p [#] eq_globs ->.
+  bypr=> &m0 @/p. 
+  rewrite Pr[mu_ge0] /= => [#] eq_globs ->.
   byequiv (: ={glob G, x} ==> ={glob G, res})=> //=.
   by proc true.
 + rnd (pred1 (psi (glob G) o)); skip=> /> &m0.
diff --git a/examples/prg-tutorial/PRGc.ec b/examples/prg-tutorial/PRGc.ec
index 605712c1e3..8b77b2961f 100644
--- a/examples/prg-tutorial/PRGc.ec
+++ b/examples/prg-tutorial/PRGc.ec
@@ -492,12 +492,13 @@ section Lemma1.
   (* We comment on the fel tactic. Its first parameter is the length
      of the initialization code. *)
   fel 1 (C_PRG.c)                       (* the query counter *)
-        (fun i=> (i + 1)%r * pr_dstate) (* probability of bad first occurring during ith query *)
+        (fun i=> (max 0 i + 1)%r * pr_dstate) (* probability of bad first occurring during ith query *)
         qN                              (* the bound on the counter (after which we stop caring) *)
         (!uniq (SRG.st::D_PRF.log))     (* the bad event *)
         []                              (* condition(s) under which the oracle(s) do not respond *)
         (size D_PRF.log = C_PRG.c).     (* general unconditional invariants *)
     (* The resulting sum is less than the specified bound *)
+    rewrite (@eq_big_seq _ (fun i=> (i + 1)%r * pr_dstate)) 1:#smt:(mem_range).
     rewrite -mulr_suml mulrAC ler_wpmul2r 1:#smt:(mu_bounded).
     rewrite (@big_reindex _ _ ([-]%Int \o ((-) 1)) ((+) 1)) 1:#smt:[ml=0].
     rewrite predTofV (@eq_bigr _ _ CoreReal.from_int) 1:#smt:[ml=0].
@@ -512,7 +513,8 @@ section Lemma1.
     by inline *; auto.
     (* Probability of bad during cth iteration is bounded by "bound c" *)
     proc=> //=; inline *; wp.
-    rnd (fun (str : state * output)=> mem D_PRF.log str.`1); auto=> /> &hr.
+    rnd (fun (str : state * output)=> mem D_PRF.log str.`1); last by move=> &hr />; smt(mu_bounded).
+    auto=> /> &hr.
     rewrite (@dprodE (mem (SRG.st::D_PRF.log){hr}) predT) dout_ll /=.
     move=> ge0_szlog ltqN_szlog st_notin_log uniq_log.
     apply/(ler_trans ((size (SRG.st::D_PRF.log){hr})%r * pr_dstate)).
diff --git a/examples/vonNeumann.eca b/examples/vonNeumann.eca
index 97d6b1b119..0cd3785549 100644
--- a/examples/vonNeumann.eca
+++ b/examples/vonNeumann.eca
@@ -102,13 +102,15 @@ while true (b2i (b = b')) 1 (2%r * p * (1%r - p))=> />.
     + by rnd (pred1 (!x)); auto.
     + by conseq ih=> />; rewrite -negbDR.
     + by rnd (pred1 x); auto=> /#.
-    by conseq ih=> /> &0 /negbDR /=.
+    conseq ih=> /> &0. 
+    rewrite ge0_mu /= => -> /#.
   + by rnd (pred1 (!x)); auto=> /#.
   + seq 1: (b' = x) _ 0%r (mu1 dbiased (!x)) (mu dvn (pred1 x \o fst)) (b <> x)=> //.
     + by auto.
     + by conseq ih=> /> &0 ->.
     + by rnd (pred1 (!x)); auto=> /#.
-    by conseq ih=> /> &0 /negbDR -> /negbDR ->.
+    conseq ih=> /> &0. 
+    rewrite ge0_mu /= => /#. 
   move=> {ih} _ -> /=; rewrite !vnE /svn /(\o)/ pred1 /= /b2i /=.
   by move: x=> [] /=; rewrite !dbiased1E /#.
 + by auto=> />; rewrite dbiased_ll.
diff --git a/src/phl/ecPhlAuto.ml b/src/phl/ecPhlAuto.ml
index 7dfe142f16..b443faca74 100644
--- a/src/phl/ecPhlAuto.ml
+++ b/src/phl/ecPhlAuto.ml
@@ -77,11 +77,18 @@ let t_auto_rnd =
 let rec t_auto_phl_r tc =
   FApi.t_seqs
     [ EcPhlWp.t_wp None;
-      FApi.t_ors [ FApi.t_seq t_auto_rnd t_auto_phl_r;
+      FApi.t_ors [ FApi.t_seq t_auto_rnd t_auto_phl_rnd_r;
                    EcPhlSkip.t_skip;
                    t_id ]]
     tc
 
+(* Recursion guard: a non-trivial [0%r <= bd] left by [bdhoare-rnd] would make
+   [t_wp] fail and [auto] silently give up on [rnd]: only recurse into phl goals. *)
+and t_auto_phl_rnd_r tc =
+  match (FApi.tc1_goal tc).f_node with
+  | FhoareS _ | FbdHoareS _ | FequivS _ -> t_auto_phl_r tc
+  | _ -> t_id tc
+
 let t_auto_phl = FApi.t_low0 "auto-phl" t_auto_phl_r
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml
index 68b95c0386..f820393dcd 100644
--- a/src/phl/ecPhlConseq.ml
+++ b/src/phl/ecPhlConseq.ml
@@ -271,33 +271,48 @@ let t_bdHoareS_conseq (pre : ss_inv) (post : ss_inv) (tc : tcenv1) =
 
 (* bdHoareF bound change rule:
  *
- *   ∀m, P m ⇒ (bd' cmp' bd)    phoare[f] P ==> Q cmp' bd'
+ *   ∀m, 0 <= bd /\ (P m ⇒ (bd' cmp' bd))    phoare[f] P ==> Q cmp' bd'
  *   ————————————————————————————————————————————————————————
  *              phoare[f] P ==> Q cmp bd
  *
  * Changes the bound and/or comparison operator. *)
 let t_bdHoareF_conseq_bd (cmp : hoarecmp) (bd : ss_inv) (tc : tcenv1) =
-  let env = FApi.tc1_env tc in
+  let hyps = FApi.tc1_hyps tc in
   let bhf = tc1_as_bdhoareF tc in
+  let env = FApi.tc1_env tc in
   let bd = ss_inv_rebind bd bhf.bhf_m in
   let mpr,_ = EcEnv.Fun.hoareF_memenv bhf.bhf_m bhf.bhf_f env in
   let bd_goal =  bd_goal tc bhf.bhf_cmp (bhf_bd bhf) cmp bd in
   let concl = f_bdHoareF (bhf_pr bhf) bhf.bhf_f (bhf_po bhf) cmp bd in
   let goal = map_ss_inv2 f_imp (bhf_pr bhf) bd_goal in
-  let bd_goal = f_forall_mems_ss_inv mpr goal in
-  FApi.xmutate1 tc `HlConseq [bd_goal; concl]
+  (* TODO: Refactor callsites so we can avoid emitting
+    `goal` if the bound does not change. *)
+  let goal = if cmp = bhf.bhf_cmp && ss_inv_alpha_eq hyps bd (bhf_bd bhf) then
+    goal
+  else
+    map_ss_inv2 f_and (map_ss_inv1 (f_real_le f_r0) (bhf_bd bhf)) goal
+ in
+  let goal = f_forall_mems_ss_inv mpr goal in
+  FApi.xmutate1 tc `HlConseq [goal; concl]
 
 (* -------------------------------------------------------------------- *)
 
 (* bdHoareS bound change rule: same as bdHoareF_conseq_bd for statements. *)
 let t_bdHoareS_conseq_bd (cmp : hoarecmp) (bd : ss_inv) (tc : tcenv1) =
+  let hyps = FApi.tc1_hyps tc in
   let bhs = tc1_as_bdhoareS tc in
   let bd = ss_inv_rebind bd (fst bhs.bhs_m) in
   let bd_goal = bd_goal tc bhs.bhs_cmp (bhs_bd bhs) cmp bd in
   let concl = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) bhs.bhs_s (bhs_po bhs) cmp bd in
-  let imp = map_ss_inv2 f_imp (bhs_pr bhs) bd_goal in
-  let bd_goal = f_forall_mems_ss_inv bhs.bhs_m imp in
-  FApi.xmutate1 tc `HlConseq [bd_goal; concl]
+  let goal = map_ss_inv2 f_imp (bhs_pr bhs) bd_goal in
+  (* TODO: Refactor callsites so we can avoid emitting
+    `goal` if the bound does not change. *)
+  let goal = if cmp = bhs.bhs_cmp && ss_inv_alpha_eq hyps bd (bhs_bd bhs) then
+    goal
+  else
+    map_ss_inv2 f_and (map_ss_inv1 (f_real_le f_r0) (bhs_bd bhs)) goal in
+  let goal = f_forall_mems_ss_inv bhs.bhs_m goal in
+  FApi.xmutate1 tc `HlConseq [goal; concl]
 
 (* -------------------------------------------------------------------- *)
 
diff --git a/src/phl/ecPhlPr.ml b/src/phl/ecPhlPr.ml
index db56dfdacd..ef7d83eec2 100644
--- a/src/phl/ecPhlPr.ml
+++ b/src/phl/ecPhlPr.ml
@@ -37,6 +37,7 @@ let t_bdhoare_ppr_r tc =
     bd in
   let pre   = ss_inv_rebind pre m in
   let concl = map_ss_inv2 f_imp pre concl in
+  let concl = map_ss_inv2 f_and (map_ss_inv1 (f_real_le f_r0) bd) concl in
   let concl = EcSubst.f_forall_mems_ss_inv (m,snd penv) concl in
   FApi.xmutate1 tc `PPR [concl]
 
diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml
index f8f7bed8a0..70a5db3054 100644
--- a/src/phl/ecPhlRnd.ml
+++ b/src/phl/ecPhlRnd.ml
@@ -212,13 +212,16 @@ module Core = struct
         let bd = {m;inv=f_local bd_id treal} in
         bd, map_ss_inv2 f_eq (bhs_bd bhs) bd, [(bd_id,GTty treal)]
     in
-    let subgoals = match tac_info, bhs.bhs_cmp with
+    let nonneg_concl =
+      f_forall_mems_ss_inv bhs.bhs_m
+        (map_ss_inv2 f_real_le {m;inv=f_r0} (bhs_bd bhs)) in
+    match tac_info, bhs.bhs_cmp with
       | PNoRndParams, FHle ->
         if is_post_indep then
           (* event is true *)
           let concl = f_bdHoareS (snd bhs.bhs_m)
             (bhs_pr bhs) s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in
-          [concl]
+          FApi.xmutate1 tc `Rnd [concl]
         else
           let event = {m; inv=mk_event ty_distr} in
           let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in
@@ -227,7 +230,9 @@ module Core = struct
           let post = POE.lift post in
           let concl = f_hoareS (snd bhs.bhs_m) pre s post in
           let concl = f_forall_simpl binders concl in
-          [concl]
+          (* the hoare post only constrains the terminating runs of [s]: also
+             require [0%r <= bd] (in every memory); closed here when trivial *)
+          FApi.t_last (FApi.t_try t_trivial) (FApi.xmutate1 tc `Rnd [concl; nonneg_concl])
       | PNoRndParams, _ ->
         if is_post_indep then
           (* event is true *)
@@ -236,7 +241,7 @@ module Core = struct
           let bounded_distr = map_ss_inv2 f_eq (map_ss_inv2 (f_mu env) distr event) f_r1 in
           let post = map_ss_inv2 f_and (bhs_po bhs) bounded_distr in
           let concl = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s post bhs.bhs_cmp (bhs_bd bhs) in
-          [concl]
+          FApi.xmutate1 tc `Rnd [concl]
         else
           let event = {m;inv=mk_event ty_distr} in
           let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) bound in
@@ -244,7 +249,7 @@ module Core = struct
           let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in
           let concl = f_bdHoareS (snd bhs.bhs_m) pre s post bhs.bhs_cmp {m;inv=f_r1} in
           let concl = f_forall_simpl binders concl in
-          [concl]
+          FApi.xmutate1 tc `Rnd [concl]
       | PSingleRndParam event, FHle ->
           let event = event ty_distr in
           let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in
@@ -253,7 +258,9 @@ module Core = struct
           let post = POE.lift post in
           let concl = f_hoareS (snd bhs.bhs_m) pre s post in
           let concl = f_forall_simpl binders concl in
-          [concl]
+          (* the hoare post only constrains the terminating runs of [s]: also
+             require [0%r <= bd] (in every memory); closed here when trivial *)
+          FApi.t_last (FApi.t_try t_trivial) (FApi.xmutate1 tc `Rnd [concl; nonneg_concl])
       | PSingleRndParam event, _ ->
           let event = event ty_distr in
           let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) bound in
@@ -261,7 +268,7 @@ module Core = struct
           let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in
           let concl = f_bdHoareS (snd bhs.bhs_m) pre s post FHeq {m;inv=f_r1} in
           let concl = f_forall_simpl binders concl in
-          [concl]
+          FApi.xmutate1 tc `Rnd [concl]
       | PMultRndParams ((phi,d1,d2,d3,d4),event), _ ->
         let event = match event ty_distr with
           | None -> {m;inv=mk_event ~simpl:false ty_distr} | Some event -> event
@@ -286,12 +293,9 @@ module Core = struct
           map_ss_inv f_ands (List.map f_inbound [d1; d2; d3; d4])
         in
         let sgoal5 = f_forall_mems_ss_inv (bhs.bhs_m) sgoal5 in
-        [bd_sgoal;sgoal1;sgoal2;sgoal3;sgoal4;sgoal5]
+        FApi.xmutate1 tc `Rnd [bd_sgoal;sgoal1;sgoal2;sgoal3;sgoal4;sgoal5]
 
       | _, _ -> tc_error !!tc "invalid arguments"
-    in
-
-    FApi.xmutate1 tc `Rnd subgoals
 
   (* -------------------------------------------------------------------- *)
   let semrnd tc mem used (s : instr list) : EcMemory.memenv * instr list =
diff --git a/src/phl/ecPhlTAuto.ml b/src/phl/ecPhlTAuto.ml
index 5abab888d0..e06514f4a0 100644
--- a/src/phl/ecPhlTAuto.ml
+++ b/src/phl/ecPhlTAuto.ml
@@ -44,6 +44,14 @@ let t_core_exfalso_r tc =
   let pre   = tc1_get_pre tc in
     if not (f_equal (inv_of_inv pre) f_false) then
       tc_error !!tc "pre-condition is not `false'";
-    FApi.xmutate1 tc `ExFalso []
+    match (FApi.tc1_goal tc).f_node with
+    | FbdHoareS bhs ->
+      FApi.xmutate1 tc `ExFalso [EcSubst.f_forall_mems_ss_inv bhs.bhs_m 
+        (map_ss_inv1 (f_real_le f_r0) (bhs_bd bhs))]
+    | FbdHoareF bhf ->
+      let (me, _) = EcEnv.Fun.hoareF_memenv (bhf.bhf_m) bhf.bhf_f (FApi.tc1_env tc) in
+      FApi.xmutate1 tc `ExFalso [EcSubst.f_forall_mems_ss_inv me 
+        (map_ss_inv1 (f_real_le f_r0) (bhf_bd bhf))]
+    | _ -> FApi.xmutate1 tc `ExFalso []
 
 let t_core_exfalso = FApi.t_low0 "core-exfalso" t_core_exfalso_r
diff --git a/tests/conseq_equiv_phoare.ec b/tests/conseq_equiv_phoare.ec
index d6383d90ea..267c0d4e6b 100644
--- a/tests/conseq_equiv_phoare.ec
+++ b/tests/conseq_equiv_phoare.ec
@@ -9,7 +9,7 @@ module M = {
 }.
 
 lemma dep_bound : phoare[M.run : M.b ==> !M.b] = (b2i M.b)%r.
-proof. by proc; auto => &hr ->. qed.
+proof. by proc; auto => &hr; rewrite le_fromint b2i_ge0 /= => ->. qed.
 
 equiv triv_equiv : M.run ~ M.run : true ==> ={M.b}.
 proof. proc; auto. qed.
diff --git a/tests/phoare-rnd-neg-bound.ec b/tests/phoare-rnd-neg-bound.ec
new file mode 100644
index 0000000000..d8fa2378e7
--- /dev/null
+++ b/tests/phoare-rnd-neg-bound.ec
@@ -0,0 +1,52 @@
+(* pHL `rnd` with an upper bound (upstream #1119): the bound check is lifted
+   into the post-condition of a hoare judgment on the statements preceding
+   the sampling, which only constrains their terminating runs. The rule must
+   also require the bound to be non-negative; under #1105 a pHL judgment
+   with a bound that is negative in some memory is false, so that goal is
+   quantified over all memories, unconditionally: after the ordinary goal,
+   `0%r <= -1%r` must remain and must be unprovable. *)
+require import AllCore Distr.
+
+module M = {
+  proc f() : unit = { var x : int; while (true) { } x <$ dunit 0; }
+}.
+
+lemma bad : phoare[M.f : true ==> true] <= (-1)%r.
+proof.
+proc.
+rnd (fun (_ : int) => true).
++ by while (true); auto.
+(* remaining goal: forall &hr, 0%r <= -1%r *)
+move=> &hr.
+fail (by smt()).
+abort.
+
+(* Same with the event inferred from the post-condition. *)
+module N = {
+  proc f() : int = { var x : int; while (true) { } x <$ dunit 0; return x; }
+}.
+
+lemma bad' : phoare[N.f : true ==> res = 0] <= (-1)%r.
+proof.
+proc.
+rnd.
++ by while (true); auto.
+(* remaining goal: forall &hr, 0%r <= -1%r *)
+move=> &hr.
+fail (by smt()).
+abort.
+
+(* Loop-free: the prefix terminates, but the bound is still negative. *)
+module L = {
+  proc f() : unit = { var y : int; var x : int; y <$ dnull; x <$ dunit 0; }
+}.
+
+lemma bad'' : phoare[L.f : true ==> true] <= (-1)%r.
+proof.
+proc.
+rnd (fun (_ : int) => true).
++ by auto=> /> y; rewrite supp_dnull.
+(* remaining goal: forall &hr, 0%r <= -1%r *)
+move=> &hr.
+fail (by smt()).
+abort.
diff --git a/theories/crypto/Birthday.eca b/theories/crypto/Birthday.eca
index df2cfb3410..e2f36de459 100644
--- a/theories/crypto/Birthday.eca
+++ b/theories/crypto/Birthday.eca
@@ -74,7 +74,8 @@ section.
     fel 1 (size Sample.l) (fun x, x%r * mu1 uT maxu) q (!uniq Sample.l) []=> //.
     + by rewrite -Bigreal.BRA.mulr_suml  Bigreal.sumidE 1:ge0_q.
     + by inline*; auto.
-    + proc;wp; rnd (mem Sample.l); skip=> // /> &hr ???.
+    + proc;wp; rnd (mem Sample.l); last by move=> &hr />; smt(size_ge0 ge0_mu1).
+      skip=> // /> &hr ???.
       apply (Mu_mem.mu_mem_le_size (Sample.l{hr}) uT (mu1 uT maxu)). 
       by move=> x _;rewrite maxuP.
     by move=> c; proc; auto=> /#.
diff --git a/theories/crypto/DiffieHellman.ec b/theories/crypto/DiffieHellman.ec
index 127b93e782..87f50a9ec2 100644
--- a/theories/crypto/DiffieHellman.ec
+++ b/theories/crypto/DiffieHellman.ec
@@ -160,9 +160,10 @@ theory List_CDH.
       seq  1: (mem s (g ^ (LCDH'.x * LCDH'.y)) /\ size s <= n) p (1%r/n%r) _ 0%r => //.
         (* The first part is dealt with by equivalence with LCDH. *)
         conseq (_: _: =p). (* strengthening >= into = for simplicity*)
+          by rewrite /= /p Pr[mu_ge0]. 
         call (_: (glob A) = (glob A){m}  ==>
                    mem res (g ^ (LCDH'.x * LCDH'.y)) /\ size res <= n)=> //.
-        bypr; progress; rewrite /p.
+        bypr; rewrite /p Pr[mu_ge0] => /> &hr gl_eq.
         byequiv (_: )=> //.
         by proc *; inline *; wp; call (_: true); auto.
       (* The second part is just arithmetic, but smt needs some help. *)
diff --git a/theories/crypto/KeyEncapsulationMechanisms.eca b/theories/crypto/KeyEncapsulationMechanisms.eca
index 57b847b08d..f3f7347f66 100644
--- a/theories/crypto/KeyEncapsulationMechanisms.eca
+++ b/theories/crypto/KeyEncapsulationMechanisms.eca
@@ -3205,10 +3205,10 @@ seq 1 : (k = kt) pr_dec_skc pr_dec_skcp _ 0%r (#pre) => //.
   rewrite Pr[mu_not] (: Pr[S.decaps(sk{m'}, c{m'}) @ &m' : true] = 1%r); 1: by byphoare S_decaps_ll => //.
   by rewrite RField.subr_eq0 eq_sym; byphoare (S_decaps_sl (glob S){m}) => //. 
 + call (: glob S = (glob S){m} /\ arg = (skt, ct) ==> res = kt); 2: by skip.
-  rewrite /pr_dec_skc; bypr => /> &m' glS.
+  rewrite /pr_dec_skc; bypr => /> &m'; rewrite Pr[mu_ge0] /= => glS.
   by byequiv => //; proc true. 
 + call (: glob S = (glob S){m} /\ arg = (skt', ct') ==> res = kt'); 2: by skip => />.
-  rewrite /pr_dec_skcp; bypr=> &m' [glS ->] /=.
+  rewrite /pr_dec_skcp; bypr=> &m'; rewrite Pr[mu_ge0] /= => -[glS ->] /=.
   by byequiv => //; proc true.
 by hoare; call (: true); skip => />. 
 qed.
diff --git a/theories/crypto/LorR.eca b/theories/crypto/LorR.eca
index 6278f76e71..1345898206 100644
--- a/theories/crypto/LorR.eca
+++ b/theories/crypto/LorR.eca
@@ -45,24 +45,28 @@ section.
     + by rewrite Pr [mu_split Aux.b].
     have -> : Pr[Aux.main(x') @ &m : res /\ Aux.b] = 1%r/2%r * Pr[L.main (x') @ &m : res].
     + byphoare (_: (glob L) = (glob L){m} /\ x = x' ==> res /\ Aux.b) => //.
-      proc; pose p := Pr[L.main(x') @ &m : res]. (* FIXME assert false without the pose *)
-      seq 1 : (Aux.b = true /\ x = x') (1%r/2%r) p  _ 0%r (glob L = (glob L){m} /\ x = x'); 1:by auto.
+      proc.
+      seq 1 : (Aux.b = true /\ x = x') (1%r/2%r) Pr[L.main(x') @ &m : res]
+        _ 0%r (glob L = (glob L){m} /\ x = x'); 1:by auto.
       + by rnd (pred1 true); skip => />; rewrite dbool1E.
-      + if; last by (conseq (_: false ==> _); 1:by smt()); auto.
+      + if; first last.
+        + (conseq (_: false ==> _) => //=; 1:by smt()); auto; progress; by rewrite Pr[mu_ge0]. 
         conseq (_ : _ ==> Aux.r) => //; 1:by smt().
         call (_: x = x' /\ glob L = (glob L){m} ==> res); last by auto.  
-        by bypr=> &m0 hm0; rewrite /p; byequiv=> //; proc (true).    
+        by bypr=> &m0; rewrite Pr[mu_ge0] /= => hm0; byequiv=> //; proc (true).    
       + by (conseq (_: _ ==> false); 1:smt()); auto.
       smt().
     have -> : Pr[Aux.main(x') @ &m : res /\ !Aux.b] = 1%r/2%r * Pr[R.main (x') @ &m : !res].
     + byphoare (_: (glob R) = (glob R){m} /\ x = x' ==> res /\ !Aux.b) => //.
-      proc; pose p := Pr[R.main(x') @ &m : !res]. 
-      seq 1 : (Aux.b = false /\ x = x') (1%r/2%r) p  _ 0%r (glob R = (glob R){m} /\ x = x'); 1:by auto.
+      proc. 
+      seq 1 : (Aux.b = false /\ x = x') (1%r/2%r) Pr[R.main(x') @ &m : !res] 
+        _ 0%r (glob R = (glob R){m} /\ x = x'); 1:by auto.
       + by rnd (pred1 false); skip => />; rewrite dbool1E.
-      + if; first by (conseq (_: false ==> _); 1:by smt()); auto.
-        conseq (_ : _ ==> !Aux.r) => //; 1:by smt().
+      + if.
+        + (conseq (_: false ==> _) => //=; 1:by smt()); auto; progress; by rewrite Pr[mu_ge0]. 
+        conseq (_ : _ ==> !Aux.r) => //=; 1:by smt().
         call (_: x = x' /\ glob R = (glob R){m} ==> !res); last by auto.
-        by bypr=> &m0 hm0; rewrite /p; byequiv=> //; proc (true). 
+        by bypr=> &m0; rewrite /p Pr[mu_ge0] => hm0; byequiv=> //; proc (true). 
       + by (conseq (_: _ ==> false); 1:smt()); auto.
       smt().
     rewrite Pr [mu_not] Hll /#.
diff --git a/theories/crypto/PROM.ec b/theories/crypto/PROM.ec
index 59fd19bc5e..f89ef3561d 100644
--- a/theories/crypto/PROM.ec
+++ b/theories/crypto/PROM.ec
@@ -301,6 +301,7 @@ fel 1 (fsize RO.m) (fun x => x%r * Pc) q (fcoll f RO.m)
   rewrite i_neq_j eq_f.
   move: i_in_mVx; rewrite i_neq_x=> /= -> /=.
   by move: j_in_mVx; rewrite j_neq_x=> /= -> /=.
+- by move=> &hr />; smt(Pc_ge0 ge0_fsize).
 - move => c; proc; auto => />; smt(get_setE fsize_set).
 - move => b c; proc; by auto.
 qed.
diff --git a/theories/crypto/RndExcept.eca b/theories/crypto/RndExcept.eca
index 56ac553c12..2d2bc32a2a 100644
--- a/theories/crypto/RndExcept.eca
+++ b/theories/crypto/RndExcept.eca
@@ -277,10 +277,11 @@ abstract theory AdversaryN.
     + rewrite BRA.sumr_const RField.intmulr count_predT.
       smt (size_range q_pos).
     + inline *;auto.
-    + proc;inline *;sp 1;if;last by hoare.
-      sp 3;wp;if;last by hoare.
+    + proc;inline *;sp 1;if; last hoare => //; smt(n_pos p_pos).
+      sp 3;wp;if;last hoare => //; smt(n_pos p_pos).
       wp;conseq (_ : _ ==> r1 \in X1)=> [ /# | ].
-      rnd;auto => &hr /> ??? Hs.
+      rnd; last by move=> &hr />; smt(p_pos n_pos).
+      auto => &hr /> ??? Hs.
       apply (ler_trans (BRA.big predT (fun (x : t) => 1%r/n%r) X{hr})).
       + apply (ler_trans _ _ _ (mu_mem_le (d i{hr}) X{hr})).
         by apply ler_sum_seq => /= ??;rewrite d_uni.
diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca
index 435ecbadcf..80d74d97ff 100644
--- a/theories/crypto/prp_prf/Strong_RP_RF.eca
+++ b/theories/crypto/prp_prf/Strong_RP_RF.eca
@@ -433,21 +433,23 @@ section CollisionProbability.
           by left; exists x0.
         by rewrite fcardU fcard1; smt(fcard_ge0).
     by auto=> />; rewrite frng0 fcards0.
-  fel 2 FEL.c (fun x, x%r * mu uD (pred1 witness)) q (ARP.coll) 
+  fel 2 FEL.c (fun x, (max 0 x)%r * mu uD (pred1 witness)) q (ARP.coll) 
            [FEL(D).FBounder.f: (FEL.c < q); FEL(D).FBounder.fi: (FEL.c < q)]
            (card (fdom ARP.m) <= FEL.c /\ card (fdom ARP.mi) <= FEL.c)=> //.
-  + rewrite -mulr_suml Bigreal.sumidE 1:ge0_q. 
+  + rewrite -mulr_suml (eq_big_seq _ (%r)); 1:smt(mem_range).
+    rewrite  Bigreal.sumidE 1:ge0_q. 
     by rewrite expr2;smt(mu_bounded ge0_q).
   + by inline*; auto=> />; rewrite fdom0 fcards0.
   + exists*FEL.c;elim*=> c.
-    conseq(:_==>_ : (c%r * mu1 uD witness))=> />.
+    conseq(:_==>_ : ((max 0 c)%r * mu1 uD witness))=> />.
+    + move => &hr; smt(ge0_mu).
     proc; sp; rcondt 1=> //.
     inline *; sp; if=> //=; last first.
-    * hoare; auto=> // /> &hr 6?.
-      by apply/RealOrder.mulr_ge0; smt(mu_bounded ge0_q).
+    * hoare; auto=> // /> &hr.
+      split => [| _ _ _ _ _ _]; smt(ge0_mu).
     sp; if=> //=.
-    * wp; rnd (rng ARP.m); skip.
-      progress.
+    * wp; rnd (rng ARP.m); last by move=> &hr />; smt(ge0_mu1).
+      skip; progress.
       - apply/(RealOrder.ler_trans ((card (frng ARP.m{hr}))%r * mu uD (pred1 witness))).
         have ->: rng ARP.m{hr} = mem (frng ARP.m{hr}).
         + by apply/fun_ext=> x; rewrite mem_frng.
@@ -464,20 +466,21 @@ section CollisionProbability.
     * by auto=> /#.
   + by move=> b c; proc; rcondf 2; auto.
   + exists*FEL.c;elim*=> c.
-    conseq(:_==>_ : (c%r * mu1 uD witness));progress.
+    conseq(:_==>_ : ((max 0 c)%r * mu1 uD witness));progress.
+    + smt(ge0_mu).
     proc; sp; rcondt 1=> //=.
     inline *; sp; if=> //=; last by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q).
     sp; if=> //=.
-    * wp; rnd (rng ARP.mi); skip.
-      progress.
+    * wp; rnd (rng ARP.mi); last by move=> &hr />; smt(ge0_mu1).
+      skip; progress.
       - apply/(RealOrder.ler_trans ((card (frng ARP.mi{hr}))%r * mu uD (pred1 witness))).
         have ->: rng ARP.mi{hr} = mem (frng ARP.mi{hr}).
         + by apply/fun_ext=> x; rewrite mem_frng.
         apply/mu_mem_le; move=> x _; have [] uD_suf [] _ uD_fu:= uD_uf_fu.
         apply/RealOrder.lerr_eq/uD_suf; 1,2:rewrite uD_fu //.
         apply: RealOrder.ler_wpmul2r.
-        + exact: ge0_mu.
-        + exact/le_fromint/(lez_trans _ _ _ (leq_card_rng_dom _)).
+        + exact: ge0_mu. search (_ <= max _ _).
+          exact/le_fromint/(lez_trans FEL.c{hr})/maxrr/(lez_trans _ _ _ (leq_card_rng_dom _)).
       - by move: H9; rewrite H1.
     * by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q).
   + move=> c; proc; rcondt 2; 1:by auto.
diff --git a/theories/distributions/Dexcepted.ec b/theories/distributions/Dexcepted.ec
index 4fe1391855..4bcaee7d47 100644
--- a/theories/distributions/Dexcepted.ec
+++ b/theories/distributions/Dexcepted.ec
@@ -97,7 +97,7 @@ qed.
 
 phoare phoare_direct x' X' P:
   [ S.direct: x = x' /\ X = X' ==> P res ] = (mu (dt x' \ X' x') P).
-proof. by bypr=> &m [] -> ->; exact/(@pr_direct &m x' X' P). qed.
+proof. bypr=> &m; rewrite ge0_mu /= => [#] -> ->; exact/(@pr_direct &m x' X' P). qed.
 
 (* -------------------------------------------------------------------- *)
 lemma pr_indirect &m x' X' P:
@@ -106,7 +106,9 @@ proof.
 byphoare (: x = x' /\ X = X' ==> _)=> //=.
 case: (forall x, (x \in dt x' => !P x) \/ !(P x /\ !X' x' x)).
 + move=> P_nsub_supp; hoare.
-  + move=> &m' [#] <<*>; rewrite eq_sym dexceptedE mulf_eq0; right.
+  + move=> &m'; split.
+    + smt(ge0_mu).
+    move => [#] <<*>; rewrite eq_sym dexceptedE mulf_eq0; right.
     rewrite mulf_eq0; left; apply/mu0_false.
     move=> x @/predI @/predC x_in_dt.
     by case: (P_nsub_supp x)=> [/(_ x_in_dt) ->|].
@@ -122,7 +124,9 @@ proc. alias 2 r0 = r.
 phoare split (mu (dt x) (predI P (predC (X' x'))))
              (mu (dt x) (X x) * mu (dt x \ X x) P)
              : (P r0 /\ !X' x' r0).
-+ move=> /= &m' [] ->> ->> {&m'}; rewrite dexceptedE.
++ move=> /= &m'; split.
+  + smt(ge0_mu).
+  move => [] ->> ->> {&m'}; rewrite dexceptedE.
   rewrite -{1}(mulr1 (mu (dt x') (predI _ _))).
   rewrite -(@divrr (weight (dt x') - mu (dt x') (X' x'))).
   + rewrite -mu_not; apply/ltr0_neq0.
@@ -150,7 +154,7 @@ qed.
 phoare phoare_indirect x' X' P:
   [ S.indirect: x = x' /\ X = X' ==> P res ]
   = (weight (dt x) * mu (dt x \ X x) P).
-proof. by bypr=> &m [] -> ->; rewrite (@pr_indirect &m x' X' P). qed.
+proof. bypr=> &m; smt(pr_indirect ge0_mu). qed.
 
 (* -------------------------------------------------------------------- *)
 lemma ll_pr_indirect &m x' X' P:
@@ -162,8 +166,7 @@ phoare ll_phoare_indirect x' X' P:
   [ S.indirect: x = x' /\ X = X' /\ is_lossless (dt x') ==> P res ]
   = (mu (dt x \ X x) P).
 proof.
-by bypr=> &m [] -> [] -> dt_ll; rewrite (@ll_pr_indirect &m x' X' P).
-qed.
+by bypr=> &m; smt(ll_pr_indirect ge0_mu). qed.
 
 (* -------------------------------------------------------------------- *)
 lemma indirect_direct &m x X P:
@@ -248,7 +251,7 @@ qed.
 
 lemma phoare_sampleE P :
   phoare [SampleE.sample : true ==> P res ] = (mu (dt i \ test i) P).
-proof. by bypr=> &m _; apply (@pr_sampleE &m i{m} test{m} P). qed.
+proof. by bypr=> &m; smt(ge0_mu pr_sampleE). qed.
 
 (* -------------------------------------------------------------------- *)
 section.
@@ -271,7 +274,7 @@ end section.
 
 phoare phoare_sampleI P :
   [ SampleI.sample : is_lossless (dt i) ==> P res ] = (mu (dt i \ test i) P).
-proof. by bypr=> &m; apply (@pr_sampleI &m i{m} test{m} P). qed.
+proof. by bypr=> &m; smt(pr_sampleI ge0_mu). qed.
 
 (* -------------------------------------------------------------------- *)
 lemma pr_sampleWi &m x y X P :
@@ -289,12 +292,12 @@ case: (X x y)=> [y_in_Xx|y_notin_Xx]; last first.
 byphoare (: i = x /\ r = y /\ test = X ==> P res)=> //; proc=> /=.
 case @[ambient]: (mu (dt x) (X x) = weight (dt x))=> Hpt.
 + hoare.
-  + by move=> />; rewrite dexceptedE Hpt.
+  + by rewrite ge0_mu => />; rewrite dexceptedE Hpt.
   while (X x r /\ i = x /\ test = X)=> //=.
   auto=> &m' [#] _ -> -> _ r; move: (mu_in_weight (X x) (dt x) r).
   by rewrite Hpt.
 conseq (: _: =(if X x r then mu (dt x \ X x) P else b2r (P r))).
-+ by move=> />; rewrite y_in_Xx.
++ smt(ge0_mu b2r_ge0). 
 conseq (_ : i = x /\ test = X ==> _) => //.
 while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x)))=> //=.
 + smt().
@@ -305,7 +308,8 @@ while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x))
   phoare split (mu (dt x) (predI P (predC (X x))))
                (mu (dt x) (X x) * mu (dt x \ X x) P)
                : (P r0 /\ !X x r0).
-  + move=> &m' [#] -> -> -> /=; rewrite dexceptedE.
+  + move=> &m'; split; 1:smt(dexceptedE ge0_mu). 
+    move => [#] -> -> -> /=; rewrite dexceptedE.
     rewrite -{1}(mulr1 (mu (dt x) (predI _ _))).
     rewrite -(@divrr (weight (dt x) - mu (dt x) (X x))).
     + smt().
@@ -327,17 +331,21 @@ while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x))
   + case: (P r0); last by conseq ih=> />.
     by hoare; conseq (: true)=> />.
   + by wp; rnd.
-  by conseq ih=> &m' />; rewrite dexceptedE.
+  by conseq ih=> &m' />; smt(ge0_mu dexceptedE).
 + by auto.
 split.
 + by move=> &m' />; rewrite mu_not #smt:(mu_bounded).
-by move=> z; conseq (: _ ==> !X x r)=> />; rnd; skip.
+move=> z; conseq (: _ ==> !X x r)=> />.
+by rnd; skip.
 qed.
 
 lemma phoare_sampleWi P :
     phoare [SampleWi.sample : is_lossless (dt i) ==> P res]
   = (if test i r then mu (dt i \ test i) P else b2r (P r)).
-proof. by bypr=> &m'; exact/(@pr_sampleWi &m' i{m'} r{m'} test{m'} P). qed.
+proof. 
+bypr=> &m'; split; 1:smt(ge0_mu b2r_ge0). 
+exact/(@pr_sampleWi &m' i{m'} r{m'} test{m'} P). 
+qed.
 
 (* -------------------------------------------------------------------- *)
 lemma pr_sampleW &m x X P :
@@ -348,18 +356,18 @@ move=> dt_ll.
 byphoare (: i = x /\ test = X ==> P res)=> //; proc=> /=.
 case @[ambient]: (mu (dt x) (X x) = weight (dt x))=> Hpt.
 + conseq (: : = 0%r)=> //.
-  + by move=> &m' _; rewrite dexceptedE Hpt.
+  + by move=> &m'; rewrite ge0_mu dexceptedE Hpt.
   seq 1 : true _ 0%r 0%r _ (i = x /\ test = X /\ X x r)=> //.
   + auto=> &m' [#] -> -> r; move: (mu_in_weight (X x) (dt x) r).
     by rewrite Hpt.
   call (: is_lossless (dt x) /\ i = x /\ test = X /\ X x r ==> P res)=> //.
-  by conseq (phoare_sampleWi P)=> // &m' [#] _ -> -> ->; rewrite dexceptedE Hpt.
+  by conseq (phoare_sampleWi P)=> // &m' /= [#] _ -> -> ->; rewrite dexceptedE Hpt.
 alias 2 r0 = r.
 (** TRANSITIVITY FOR PHOARE!! **)
 phoare split (mu (dt x) (predI P (predC (X x))))
              (mu (dt x) (X x) * mu (dt x \ X x) P)
              : (P r0 /\ !X x r0).
-+ move=> &m' _ /=; rewrite dexceptedE.
++ move=> &m'; rewrite ge0_mu /= dexceptedE => _.
   rewrite -{1}(mulr1 (mu (dt x) (predI _ _))).
   rewrite -(@divrr (weight (dt x) - mu (dt x) (X x))).
   + smt().
@@ -387,7 +395,7 @@ qed.
 
 phoare phoare_sampleW P :
   [ SampleW.sample: is_lossless (dt i) ==> P res ] = (mu (dt i \ test i) P).
-proof. by bypr=> &m; exact/(@pr_sampleW &m i{m} test{m} P). qed.
+proof. bypr=> &m; rewrite ge0_mu /= => ll; exact(@pr_sampleW &m i{m} test{m} P). qed.
 
 (* -------------------------------------------------------------------- *)
 equiv sampleE_sampleI : SampleE.sample ~ SampleI.sample :
@@ -506,7 +514,7 @@ proof. by rewrite (@sampleE_fixed &m x P) (@WS.pr_sampleE &m x test P). qed.
 
 phoare phoare_sampleE P :
   [ SampleE.sample : true ==> P res ] = (mu (dt i \ test i) P).
-proof. by bypr=> &m _; exact/(@pr_sampleE &m i{m} P). qed.
+proof. by bypr=> &m; rewrite ge0_mu /=; exact/(@pr_sampleE &m i{m} P). qed.
 
 (* -------------------------------------------------------------------- *)
 local lemma sampleI_fixed &m x P :
@@ -529,7 +537,7 @@ qed.
 
 phoare phoare_sampleI P :
   [ SampleI.sample: is_lossless (dt i) ==> P res ] = (mu (dt i \ test i) P).
-proof. bypr=> &m; exact/(@pr_sampleI &m i{m} P). qed.
+proof. bypr=> &m; rewrite ge0_mu; exact/(@pr_sampleI &m i{m} P). qed.
 
 (* -------------------------------------------------------------------- *)
 local lemma sampleWi_fixed &m x y P :
@@ -553,7 +561,7 @@ qed.
 phoare phoare_sampleWi P :
   [ SampleWi.sample : is_lossless (dt i) ==> P res ]
   = (if test i r then mu (dt i \ test i) P else b2r (P r)).
-proof. by bypr=> &m; exact/(@pr_sampleWi &m i{m} r{m} P). qed.
+proof. by bypr=> &m; split; [smt(ge0_mu b2r_ge0)|]; exact/(@pr_sampleWi &m i{m} r{m} P). qed.
 
 (* -------------------------------------------------------------------- *)
 local lemma sampleW_fixed &m x P :
@@ -576,7 +584,7 @@ qed.
 
 phoare phoare_sampleW P :
   [ SampleW.sample: is_lossless (dt i) ==> P res ] = (mu (dt i \ test i) P).
-proof. by bypr=> &m; exact/(@pr_sampleW &m i{m} P). qed.
+proof. by bypr=> &m; rewrite ge0_mu; exact/(@pr_sampleW &m i{m} P). qed.
 
 (* -------------------------------------------------------------------- *)
 equiv sampleE_sampleI : SampleE.sample ~ SampleI.sample :
diff --git a/theories/encryption/Means.ec b/theories/encryption/Means.ec
index 7ba0edb18c..7aafa5a195 100644
--- a/theories/encryption/Means.ec
+++ b/theories/encryption/Means.ec
@@ -33,9 +33,8 @@ proc.
 seq 1: (v = x) (mu1 d v) pr 1%r 0%r ((glob A) = (glob A){m})=> //.
 + by rnd.
 + by rnd; auto=> />; rewrite pred1E.
-+ call (: (glob A) = (glob A){m} /\ x = v
-          ==> ev v (glob A) res)=> //.
-  rewrite /pr; bypr=> /> &0 eqGlob.
++ call (: (glob A) = (glob A){m} /\ x = v ==> ev v (glob A) res)=> //.
+  rewrite /pr; bypr => &0; rewrite Pr[mu_ge0] => eqGlob />.
   by byequiv (: ={glob A, x} ==> ={res, glob A})=> //; proc true.
 by hoare => /=; call (: true); auto=> /#.
 qed.
diff --git a/theories/modules/EventPartitioning.ec b/theories/modules/EventPartitioning.ec
index 4939f847eb..ff89b559b1 100644
--- a/theories/modules/EventPartitioning.ec
+++ b/theories/modules/EventPartitioning.ec
@@ -234,7 +234,8 @@ abstract theory SubuniformReference.
     => Pr[M.f(i) @ &m: res = a] = (k i)/(size (undup (X i)))%r.
   proof.
   move=> support_M a_in_X; have <-: Pr[M.f(i) @ &m: true] = (k i).
-  + by byphoare (_: arg = i ==> true)=> //=; conseq weight_M.
+  + byphoare (_: arg = i ==> true)=> //=; conseq weight_M => />.
+    apply/ltrW/gt0_k.
   rewrite (@subuniform_result M M_suf i X a &m support_M a_in_X) mulrAC divff //.
   rewrite eq_fromint size_eq0 undup_nilp -implybF=> h.
   by move: a_in_X; rewrite h.
diff --git a/theories/modules/PlugAndPray.eca b/theories/modules/PlugAndPray.eca
index b6a721858f..14e9056eac 100644
--- a/theories/modules/PlugAndPray.eca
+++ b/theories/modules/PlugAndPray.eca
@@ -40,7 +40,7 @@ seq  1: (phi (glob G) o)
         _ 0%r => //.
   (* FIXME: This is more verbose than it should be! *)
 + call (: (glob G) = (glob G){m} /\ x = x0 ==> phi (glob G) res) => //.
-  bypr=> &m0 @/p [#] eq_globs ->.
+  bypr=> &m0 @/p; rewrite Pr[mu_ge0] => [#] [] eq_globs ->.
   byequiv (: ={glob G, x} ==> ={glob G, res})=> //=.
   by proc true.
 + rnd (pred1 (psi (glob G) o)); skip=> /> &m0 hphi.
diff --git a/theories/modules/TotalProb.ec b/theories/modules/TotalProb.ec
index c513cc7d7f..22401c5642 100644
--- a/theories/modules/TotalProb.ec
+++ b/theories/modules/TotalProb.ec
@@ -89,7 +89,7 @@ seq 1 :
 + by auto.
 + by rnd (pred1 x'); auto.
 + call (: i = i' /\ x = x' /\ glob M = (glob M){m} ==> res).
-  + bypr => &hr [#] -> -> glob_eq.
+  + bypr => &hr; rewrite Pr[mu_ge0] /= => [#] -> -> glob_eq.
     by byequiv (: ={i, x, glob M} ==> ={res}) => //; sim.
 + by auto.
 by hoare; call (: true); auto; smt().