>>444
printf("\\10000 %1d\n",a/10000);
a %= 10000;
printf("\\5000 %1d\n",a/5000);
a %= 5000;