theorem :: QUATERN3:42

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