Theorem Nat.prod_pow_factorization_choose

Modification history