There is a paper by Vincent Lefèvre that indeed proves that floating point division and a floor implement the euclidean division, with a careful analysis of when. [1] A corollary of the main theorem in the paper is that, with round to nearest, if x and y fit in 53 bits unsigned then it works out.
[1] https://hal.univ-lorraine.fr/inria-00070403v1