>>856-857
大昔のPutnumに、これより弱い不等式があったよね。

>>885
Moreau's inequality が思い浮かぶと同時に、一松先生を思い出す。(謎掛け)