Return division via inverse element axioms

[ElijahVlasov]

If a division a / b appears in an annotation horus-compile will change it to a * inverse_b for some fresh inverse_b and add additional field axiom with a s-expression stating that inverse_b is the inverse of b.