Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic. - David Monniaux; Alice Pain (ARITH, 2022)