let p, q, s, t be Real; :: thesis: ( p > 0 & p * s < 0 implies ( ((p * t) - (q * s)) / (p - s) < 0 iff - (q / p) > - (t / s) ) )
assume that
A0: p > 0 and
A2: p * s < 0 ; :: thesis: ( ((p * t) - (q * s)) / (p - s) < 0 iff - (q / p) > - (t / s) )
A4: s < 0 by A0, A2;
thus ( ((p * t) - (q * s)) / (p - s) < 0 implies - (q / p) > - (t / s) ) :: thesis: ( - (q / p) > - (t / s) implies ((p * t) - (q * s)) / (p - s) < 0 )

proof

assume A3: ((p * t) - (q * s)) / (p - s) < 0 ; :: thesis: - (q / p) > - (t / s)
p - s > 0 by Le1, A0, A2;
then (p * t) - (q * s) < 0 by A3;
then ((p * t) - (q * s)) - (p * t) < 0 - (p * t) by XREAL_1:9;
then ((- p) * t) / s < ((- q) * s) / s by A4, XREAL_1:75;
then ((- p) * t) / s < (- q) * (s / s) by XCMPLX_1:74;
then - q > ((- p) * t) / s by A4, XCMPLX_1:88;
then (- q) / p > (((- p) * t) / s) / p by A0, XREAL_1:74;
then (- q) / p > ((t / s) * (- p)) / p by XCMPLX_1:74;
then (- q) / p > (t / s) * ((- p) / p) by XCMPLX_1:74;
then (- q) / p > (t / s) * (- (p / p)) by XCMPLX_1:187;
then - (q / p) > - ((t / s) * (p / p)) by XCMPLX_1:187;
hence - (q / p) > - (t / s) by XCMPLX_1:88, A0; :: thesis: verum

end;

assume - (q / p) > - (t / s) ; :: thesis: ((p * t) - (q * s)) / (p - s) < 0
then (- (q / p)) * p > (- (t / s)) * p by XREAL_1:68, A0;
then ((- q) / p) * p > - ((t / s) * p) by XCMPLX_1:187;
then - q > (- (t / s)) * p by XCMPLX_1:87, A0;
then ((- (t / s)) * p) * s > (- q) * s by XREAL_1:69, A4;
then ((- (t / s)) * s) * p > (- q) * s ;
then (((- t) / s) * s) * p > (- q) * s by XCMPLX_1:187;
then (- t) * p > (- q) * s by XCMPLX_1:87, A4;
then A8: ((- t) * p) - ((- t) * p) > ((- q) * s) - ((- t) * p) by XREAL_1:9;
p - s > 0 by Le1, A0, A2;
hence ((p * t) - (q * s)) / (p - s) < 0 by A8; :: thesis: verum