for r1, r2, r3 being non negative Real holds
( not r1 * r2 <= r3 or r1 <= sqrt r3 or r2 <= sqrt r3 )