require import AllCore Distr DBool.

module M = {
  proc run() : bool = {
    var b;
    b <$ {0,1};
    return b;
  }
}.

module N = {
  proc run() : bool = {
    var b;
    b <$ {0,1};
    return b;
  }
}.

phoare M_bound : [M.run : true ==> res] = (1%r / 2%r).
proof.
proc.
rnd.
skip => /=.
apply dboolE.
qed.

equiv N_M_equiv : N.run ~ M.run : true ==> res{1} <=> res{2}.
proof.
sim.
qed.

phoare N_bound : [N.run : true ==> res] = (1%r / 2%r).
proof.
conseq N_M_equiv M_bound => //.
qed.