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