theorem :: QUATERN3:38

for z1, z2 being Quaternion holds |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2