Metamath Proof Explorer


Syntax definition cmpq

Description: Positive pre-fraction multiplication.

Ref Expression
Assertion cmpq
class .pQ