Theorem Nat.mul_lt_mul_pow_succ

Modification history