Rollup merge of #156647 - oscargus:fasterfloatmidpoint, r=SimonSapin

Change division to multiplication in floating-point midpoint

Multiplication is faster than division on most (all?) platforms. While the optimizer will handle this, there is really no point in relying on that. Using multiplication directly will not have any drawbacks and are numerically identical (in this case since 1.0 / 2.0 == 0.5)

Consider the examples at https://godbolt.org/z/oMvb9vobG where it is clear that the non-optimized version uses division, while the optimized version uses multiplication.