An exact proof term for the current goal is CSNo_ReIm_split z w (complex_CSNo z Hz) (complex_CSNo w Hw).