proveit.numbers.
simplified_numeric_rational
Given a numerator and a denominator as integers, return an Expression of the equivalent irreducible rational.