(bvsge s t) abbreviates (bvsle t s)