for x, y being Complex holds 2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2) by Lm20;