I just tried it with several different denominators & always get a result in the range of 34 microseconds. So floating point division is about 3-4 times slower than multiplication (9 usec).
Even so, that's about 30,000 divisions per second. This seems fast enough for (much) government work! :
Hey, I work for the government 
34 microseconds is amazing. I originally tried to do my current project on a pic16F, and was getting results about a thousand times slower. It was at the point where I was trying to use 2 PICs, one basically as a floating-point processor, and the whole project got kludgy. Not to mention all the fun I had learning how to do floating point division in assembly on a processor that only does 8-bit integer add and subtract.
Because of the speed, it just works on the Ardunio. And the HLL is so much faster than messing around with assembly or JAL. What took me weeks on the PIC took an hour on the Arduino.
I would tend to believe what the compiler is reporting, but I just posted something on this in Bugs/Suggestions, so we will see.
I saw your post there, I'm looking forward to seeing the answer. If we trust the compiler, there's no difference beween float and double though. Float is good enough for my purposes though.