let p be Rational; :: thesis: ( p <= 1 iff numerator p <= denominator p )

A1: now

assume A2: p <= 1 ; :: thesis: numerator p <= denominator p

per cases ( p = 1 or p < 1 ) by A2, XXREAL_0:1;

suppose p = 1 ; :: thesis: numerator p <= denominator p

hence numerator p <= denominator p ; :: thesis: verum

end;

suppose p < 1 ; :: thesis: numerator p <= denominator p

hence numerator p <= denominator p by Th72; :: thesis: verum

end;

end;

end;

now

assume A3: numerator p <= denominator p ; :: thesis: p <= 1

per cases ( numerator p = denominator p or numerator p < denominator p ) by A3, XXREAL_0:1;

suppose numerator p = denominator p ; :: thesis: p <= 1

hence p <= 1 by Th47; :: thesis: verum

end;

suppose numerator p < denominator p ; :: thesis: p <= 1

hence p <= 1 by Th72; :: thesis: verum

end;

end;

end;

hence ( p <= 1 iff numerator p <= denominator p ) by A1; :: thesis: verum