Core version division_ring_has_div erratically requires two instances of division_ring

Embed an element of a division ring into the unit group. By combining this function with the operations on units, or the /ₚ operation, it is possible to write a division as a partial function with three arguments.