let x be Real; :: thesis: ( sin x <> 0 implies cot (2 * x) = (((cot x) ^2) - 1) / (2 * (cot x)) )
assume A1: sin x <> 0 ; :: thesis: cot (2 * x) = (((cot x) ^2) - 1) / (2 * (cot x))
cot (2 * x) = cot (x + x)
.= (((cot x) * (cot x)) - 1) / ((cot x) + (cot x)) by A1, SIN_COS4:9
.= (((cot x) * (cot x)) - 1) / (2 * (cot x)) ;
hence cot (2 * x) = (((cot x) ^2) - 1) / (2 * (cot x)) ; :: thesis: verum