Theorem Nat.factorization_le_factorization_mul_right

Modification history