(bvsgt s t) abbreviates (bvslt t s)