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 Th64; :: 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 Th48; :: thesis: verum

end;

suppose numerator p < - (denominator p) ; :: thesis: p <= - 1

hence p <= - 1 by Th64; :: thesis: verum

end;

end;

end;

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