proposition: Lemma prime_decompE n : prime_decomp n = [seq (p, logn p n) | p <- primes n].
proof: Proof. case: n => // n; pose f0 := (0, 0); rewrite -map_comp. apply: (@eq_from_nth _ f0) => [|i lt_i_n]; first by rewrite size_map. rewrite (nth_map f0) //; case def_f: (nth _ _ i) => [p e] /=. congr (_, _); rewrite [n.+1]prod_prime_decomp //. have: (p, e) \in prime_decomp n.+1 by rewrite -def_f mem_nth. case/mem_prime_decomp=> pr_p _ _. rewrite (big_nth f0) big_mkord (bigD1 (Ordinal lt_i_n)) //=. rewrite def_f mulnC logn_Gauss ?pfactorK //. apply big_ind => [|m1 m2 com1 com2| [j ltj] /=]; first exact: coprimen1. by rewrite coprimeMr com1. rewrite -val_eqE /= => nji; case def_j: (nth _ _ j) => [q e1] /=. have: (q, e1) \in prime_decomp n.+1 by rewrite -def_j mem_nth. case/mem_prime_decomp=> pr_q e1_gt0 _; rewrite coprime_pexpr //. rewrite prime_coprime // dvdn_prime2 //; apply: contra nji => eq_pq. rewrite -(nth_uniq 0 _ _ (primes_uniq n.+1)) ?size_map //=. by rewrite !(nth_map f0) // def_f def_j /= eq_sym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)