sS dropLeadingNumberAndDot_trim(S s) {
  int i = indexOf(s, '.');
  if (i < 0) ret s;
  if (isInteger(takeFirst(i, s))) ret trimSubstring(s, i+1);
  ret s;
}