Format microseconds as hours:minutes:seconds, etc The following is inspired by a question that came up on Stack&nbsp;Overflow today.

Given a number of microseconds, 0 &lt;= n &lt;= 86400000000 (e.g. 12345678900), output a formatted string hh:mm:ss:000:000, e.g. 03:25:45:678:900.

          0 -&gt; '00:00:00:000:000'
12345678900 -&gt; '03:25:45:678:900'
86400000000 -&gt; '24:00:00:000:000'


I have a solution in Python in 209 bytes, but can it go lower?
Python 2, 82 79 bytes

n=input()
o=""
for k in[1000]*2+[60]*3:o=":%0*d"%(k%7/2,n%k)+o;n/=k
print o[1:]


Builds the string, iterating through a series of divmods. The only fancy bit is the %7/2, which maps 1000 -&gt; 3 and 60 -&gt; 2.