Theorem Nat.mul_self_lt_mul_self

Modification history