Theorem ne_top_of_lt

Modification history