for p, q being Rational holds
( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) )