pHL while (>=, variant form) never requires bd <= 1 at loop exit #1127

The lower-bound while inv vrnt k eps rule (t_bdhoare_while_rev_geq_r) only emits !Q => bd = 0%r for the loop-exit case; when the loop exits with Q the probability is 1, but nothing requires bd <= 1%r. With a loop that is never entered every other obligation is vacuous, so phoare[...] >= 2%r is provable and contradicts Pr[...] = 1%r. This is not a negative-bound issue (#1100-#1102) and is not addressed by #1105, which only adds 0 <= bd.

MRE:

require import AllCore.

module M = { proc f() : unit = { while (false) {} } }.

lemma f_bad : phoare[M.f : true ==> true] >= 2%r.
proof.
proc.
while (true) 0 0 1%r.
+ done.
+ done.
+ done.
+ by move=> _; exfalso.
+ by exfalso.
+ split; first done.
  by move=> z; exfalso.
qed.

lemma bad &m : false.
proof.
have h1 : Pr[M.f() @ &m : true] = 1%r by byphoare => //; proc; rcondf 1; auto.
have h2 : 2%r <= Pr[M.f() @ &m : true] by byphoare f_bad.
smt().
qed.

Root cause: src/phl/ecPhlWhile.ml, t_bdhoare_while_rev_geq_r, pre_bound_concl (l. 240-250): the FHeq case checks bd = if Q then 1%r else 0%r, the FHge case only !Q => bd = 0%r (since the 2022 rewrite 70ac960). For FHge the rule should emit (Q => bd <= 1%r) /\ (!Q => bd = 0%r).