`byupto` assumes that the bad event is monotonic without checks

[oskgo]

MRE:

module Foo = {
  var b: bool

  proc p() = {
    b <- true;
  }

  proc q() = {
    b <- true;
    b <- false;
  }
}.

lemma L &m: Pr[Foo.p() @&m: !Foo.b] = Pr[Foo.q() @&m: !Foo.b].
proof.
byupto.
qed.

weaponization:

require import Real.

lemma LT &m: Pr[Foo.p() @&m: !Foo.b] = 0%r.
proof. byphoare => //; hoare; proc; auto. qed.

lemma LF &m: Pr[Foo.q() @&m: !Foo.b] = 1%r.
proof. byphoare => //; proc; auto. qed.

lemma F: false.
proof.
suff: forall &m, 0%r = 1%r by done.
move => &m; rewrite -(LT &m) -(LF &m).
apply (L &m).
qed.