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 whe

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 https://hal.univ-lorraine.fr/inria-00070403v1