pHL seq permits negative probabilities

[oskgo]

The pHL seq rule as documented in the refman is only sound for positive probabilities. More specifically we run into problems for the (<=) and (>=) cases, but not the (=) case.

MRE:

require import Real Distr.

module M = {proc p() = {}}.

lemma le0: phoare[M.p: true ==> true] <= 0%r.
proof.
proc.
by seq 0: (true) 1%r 1%r 1%r (-1%r).
qed.

module M' = {proc p() = {var r: bool; r <$ dnull;}}.

lemma ge2: phoare[M'.p: true ==> true] >= 2%r.
proof.
proc.
seq 0: (true) _ 0%r (-2%r) (-1%r) => //.
- hoare.
  + smt().    
  auto.
- auto.
smt().
qed.

Related to #1096.