(bvugt s t) abbreviates (bvult t s)