Theorem posMulStrictMono_iff_posMulReflectLE

Modification history