Theorem normalize_mul

Modification history