let a, b be Real; ( 0 <= a & (b - a) * (b + a) < 0 implies ( - a < b & b < a ) )
assume that
A1:
a >= 0
and
A2:
(b - a) * (b + a) < 0
; ( - a < b & b < a )
A3:
( ( b - a > 0 & b + a < 0 ) or ( b - a < 0 & b + a > 0 ) )
by A2, Lm35;
then A4:
b < a + 0
by A1, Lm16;
b + 0 <= b + a
by A1, Lm6;
then
b > 0 - a
by A1, A3, Lm17;
hence
( - a < b & b < a )
by A4; verum