theorem :: QUATERN3:43

for z1, z2 being Quaternion st |.z1.| - |.z2.| <> 0 holds
((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0