This fixes #212 and implements a version of the pHL while rule which
does have a(n unpublished) pen-and-paper proof.

This (obviously) makes using the pHL while rule generally less simple,
but particularly so when the loop condition itself is probabilistically
modified by the loop body (as, for example, in rejection sampling). In
general, the bound given to the `while` tactic in those cases will need
to be conditional. (Essentially capturing control-flow conditions in the
bound itself.)

Examples of proofs illustrating this case can be found in
theories/distributions/Dexcepted.ec (starting line 299, including the
conseq) and examples/PIR.ec (starting line 202, including also the
conseq).

Upper-bounds should be unaffected.

On lower bounds, one can no longer apply the upper bound rule.

On equalities, we have now added the lower-bound exit check (that if the
loop is not entered and the event is true, then the probability should
be 1), and further missing checks.

In all cases, the inductive reasoning case was simplified to remove
duplicated control-flow.

co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr>
co-authored-by: François Dupressoir <fdupress@gmail.com>