environ
vocabularies HIDDEN, NUMBERS, SIN_COS, CARD_1, SIN_COS4, ARYTM_3, RELAT_1, ARYTM_1, SQUARE_1, NEWTON, COMPLEX1, XXREAL_0, REAL_1, SIN_COS2, FUNCT_1, SIN_COS5;
notations HIDDEN, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, SIN_COS4, SIN_COS, NEWTON, NAT_1, SIN_COS2, XXREAL_0;
definitions ;
theorems XCMPLX_1, SIN_COS, SIN_COS4, SQUARE_1, NEWTON, ABSVALUE, SIN_COS2, COMPLEX1, XREAL_1, XXREAL_0;
schemes ;
registrations XREAL_0, SQUARE_1, MEMBERED, NEWTON, SIN_COS, VALUED_0, RELSET_1, SIN_COS2;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_1, BINOP_2, SIN_COS, SIN_COS2, SIN_COS4, VALUED_1, NEWTON;
requirements HIDDEN, REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
equalities SQUARE_1, SIN_COS4;
expansions ;
Lm1:
for x being Real holds coth (- x) = - (coth x)
Lm2:
for x being Real holds (cosh . x) ^2 = 1 + ((sinh . x) ^2)
Lm3:
for x being Real holds ((cosh . x) ^2) - 1 = (sinh . x) ^2
Lm4:
for x being Real st x > 0 holds
sinh x >= 0