let x be Real; :: thesis: ( sin (x / 2) <> 0 implies cot (x / 2) = (sin x) / (1 - (cos x)) )

assume sin (x / 2) <> 0 ; :: thesis: cot (x / 2) = (sin x) / (1 - (cos x))

then A1: 2 * (sin (x / 2)) <> 0 ;

(sin x) / (1 - (cos x)) = ((2 * (sin (x / 2))) * (cos (x / 2))) / (1 - (cos (2 * (x / 2)))) by Th5

.= ((2 * (sin (x / 2))) * (cos (x / 2))) / (1 - (1 - (2 * ((sin (x / 2)) ^2)))) by Th7

.= ((2 * (sin (x / 2))) * (cos (x / 2))) / ((2 * (sin (x / 2))) * (sin (x / 2)))

.= (cos (x / 2)) / (sin (x / 2)) by A1, XCMPLX_1:91 ;

hence cot (x / 2) = (sin x) / (1 - (cos x)) ; :: thesis: verum

assume sin (x / 2) <> 0 ; :: thesis: cot (x / 2) = (sin x) / (1 - (cos x))

then A1: 2 * (sin (x / 2)) <> 0 ;

(sin x) / (1 - (cos x)) = ((2 * (sin (x / 2))) * (cos (x / 2))) / (1 - (cos (2 * (x / 2)))) by Th5

.= ((2 * (sin (x / 2))) * (cos (x / 2))) / (1 - (1 - (2 * ((sin (x / 2)) ^2)))) by Th7

.= ((2 * (sin (x / 2))) * (cos (x / 2))) / ((2 * (sin (x / 2))) * (sin (x / 2)))

.= (cos (x / 2)) / (sin (x / 2)) by A1, XCMPLX_1:91 ;

hence cot (x / 2) = (sin x) / (1 - (cos x)) ; :: thesis: verum