Theorem cmp_eq_lt_iff

Modification history