List of theorems referencing the symbol FR_IS_NONNEG


(575) Theorem 426: [?] (X in Fr) •imp (Fr_is_nonneg(X) •eq Fr_is_nonneg([S_Rev(car(X)),S_Rev(cdr(X))]))
(576) Theorem 427: [?] ((X in Fr) & (Y in Fr) & Same_frac(X,Y)) •imp (Fr_is_nonneg(X) •eq Fr_is_nonneg(Y))