/* apply the definition of `cosh` */
  ( e^ln(c+sqrt(c^2-1)) + e^( -ln(c+sqrt(c^2-1)) ) )/2
    /* apply `e^(-x) = frac(1)(e^x)` and (since `c+sqrt(c^2-1) >= 1` since `c>=1`)
      `e^(ln x) = x` */
= ( c+sqrt(c^2-1) + 1/(c+sqrt(c^2-1)) )/2
    /* multiply both sides of the latter with `c-sqrt(c^2-1)`,
       move `frac(1)(2)` to the front */
= 1/2 (c+sqrt(c^2-1)) + 1/2 (c-sqrt(c^2-1)) / ( (c-sqrt(c^2-1)) (c+sqrt(c^2-1)) )
    /* apply `(a-b)(a+b) = a^2-b^2` */
= 1/2 (c+sqrt(c^2-1)) + 1/2 (c-sqrt(c^2-1)) / ( c^2 - (sqrt(c^2-1))^2 )
    /* `c^2 - 1 >= 0` since `c>=1`, so apply `(sqrt(x))^2 = x` */
= 1/2 (c+sqrt(c^2-1)) + 1/2 (c-sqrt(c^2-1)) / ( c^2 - (c^2 - 1) )
    /* simplify the latter divisor */
= 1/2 (c+sqrt(c^2-1)) + 1/2 (c-sqrt(c^2-1)) / 1
   /* remove division by `1` */
= 1/2 (c+sqrt(c^2-1)) + 1/2 (c-sqrt(c^2-1))
   /* combine similar terms, `sqrt` terms cancel out */
= 1/2 ( 2c ) = c