proposition: Lemma mem_prime_decomp n p e : (p, e) \in prime_decomp n -> [/\ prime p, e > 0 & p ^ e %| n].
proof: Proof. case: (posnP n) => [-> //| /prime_decomp_correct[def_n mem_pd ord_pd pd_pe]]. have /andP[pr_p ->] := allP mem_pd _ pd_pe; split=> //; last first. case/splitPr: pd_pe def_n => pd1 pd2 ->. by rewrite big_cat big_cons /= mulnCA dvdn_mulr. have lt1p: 1 < p. apply: (allP (order_path_min ltn_trans ord_pd)). by apply/mapP; exists (p, e). apply/primeP; split=> // d dv_d_p; apply/norP=> [[nd1 ndp]]. case/hasP: pr_p; exists d => //. rewrite mem_index_iota andbC 2!ltn_neqAle ndp eq_sym nd1. by have lt0p := ltnW lt1p; rewrite dvdn_leq // (dvdn_gt0 lt0p). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)