Interesting setup @sjakobi. Equality would be the missing part here (unless I missed the equality function) but it seems like this could be encoded using your common denominator function. Or alternatively xⁿ * yᵈ = yⁿ * xᵈ -> xⁿ/xᵈ ≡ yⁿ/yᵈ.
I have added
equal and a few other functions. Documentation is still rather lacking but feel free to give it a try.