let x be Real; :: thesis: ( x <= 0 implies sinh x <= 0 )
assume A1: x <= 0 ; :: thesis: sinh x <= 0

per cases ( x < 0 or x = 0 ) by A1, XXREAL_0:1;

suppose A2: x < 0 ; :: thesis: sinh x <= 0

then - x > 0 by XREAL_1:58;
then A3: exp_R . (- x) >= 1 by SIN_COS:52;
exp_R . x <= 1 by A2, SIN_COS:53;
then (exp_R . x) - (exp_R . (- x)) <= 1 - 1 by A3, XREAL_1:13;
then ((exp_R . x) - (exp_R . (- x))) / 2 <= 0 by XREAL_1:138;
then sinh . x <= 0 by SIN_COS2:def 1;
hence sinh x <= 0 by SIN_COS2:def 2; :: thesis: verum

end;

suppose x = 0 ; :: thesis: sinh x <= 0

hence sinh x <= 0 by SIN_COS2:16, SIN_COS2:def 2; :: thesis: verum

end;

end;