(bvuge s t) abbreviates (or (bvult t s) (= s t))