proposition: Lemma prod_prime_decomp n : n > 0 -> n = \prod_(f <- prime_decomp n) f.1 ^ f.2.
proof: Proof. by case/prime_decomp_correct. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)