An exact proof term for the current goal is complex_quaternion 0 complex_0.