Theorem Nat.mul_self_le_mul_self

Modification history