Theorem left_ne_mul

Modification history