for p being Real holds cosh . p >= 1