theorem :: QUATERN3:40

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