Theorem mul_add_one

Modification history