Theorem Nat.factorization_le_factorization_mul_left

Modification history