theorem :: QUATERN3:69

for z1, z2, z3 being Quaternion holds z3 * (z1 - z2) = (- z3) * (z2 - z1)