Metamath Proof Explorer


Syntax definition cpp

Description: Positive real addition.

Ref Expression
Assertion cpp class +P