This patch replaces three different pre-existing implementations of div[sdt]f3 LibCalls with a generic one - like it is already done for many other LibCalls.
The patch was written with intent of the proof being as self-contained as possible, so future contributors do not have to re-prove it again. On the other hand, this may make it look somewhat cluttered, so feedback on both correctness and readability is highly appreciated.
When fuzzing with AFL++ (25M iterations each type width), just one error was found: for single precision, 0x1.fffffep-126F divided by 2.F was not correctly rounded to exactly 1.0. On the other hand, this patch is just an intentionally simplified version of the full patch introducing a proper support for subnormal results - the full version fixes this issue as well.
This particular diff pretends to be an NFC refactoring and technically the above issue is not a regression because the original implementation yields the same result. :)