let x be Real; :: thesis: ( cos (x / 2) <> 0 implies cot (x / 2) = (1 + (cos x)) / (sin x) )
assume cos (x / 2) <> 0 ; :: thesis: cot (x / 2) = (1 + (cos x)) / (sin x)
then A1: 2 * (cos (x / 2)) <> 0 ;
(1 + (cos x)) / (sin x) = (1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / (sin (2 * (x / 2))) by Th7
.= (2 * ((cos (x / 2)) * (cos (x / 2)))) / ((2 * (sin (x / 2))) * (cos (x / 2))) by Th5
.= ((2 * (cos (x / 2))) * (cos (x / 2))) / ((2 * (cos (x / 2))) * (sin (x / 2)))
.= cot (x / 2) by A1, XCMPLX_1:91 ;
hence cot (x / 2) = (1 + (cos x)) / (sin x) ; :: thesis: verum