This fixes Jessie3 proving less VCs than Jessie2 on the float_sqrt example.

Only one pattern has been added to Why3 for now; Why2 knows about three
other variations (commutativity of the two multiplications).

The pattern mechanism used by the Gappa printer could possibly be
generalized and live on its own, hopefully with some kind of parser so that
one does not have to build patterns by hand.