Why3.v 110 Bytes