The close runner up for "most fun part": integer division

We leave in all ".0" which make no difference on py3 (nor on py2 with a
future import) but are necessary on py2, and we add in int() where
necessary to make py3 behave like py2.

Two minor "exceptions":
- We add in a comment where the code makes sure that we divide floats
  (so that py2 does not need an extra float() or .0) but where this is
  hard to spot.
- We let FormatTime convert its argument to int. Apparantly, the code
  expected to be fed an int on py2 but would break if not. So, it is
  more robust on py2 now and equivalent otherwise.