Theorem cmp_compares

Modification history