An exact proof term for the current goal is quaternion_octonion 0 quaternion_0.