let p, s be Real; :: thesis: ( p > 0 & p * s < 0 implies p - s > 0 )
assume that
A0: p > 0 and
A1: p * s < 0 ; :: thesis: p - s > 0
s < 0 / p by A0, A1;
hence p - s > 0 by A0; :: thesis: verum