proposition: Lemma divisors_correct n : n > 0 -> [/\ uniq (divisors n), sorted leq (divisors n) & forall d, (d \in divisors n) = (d %| n)].
proof: Proof. move/prod_prime_decomp=> def_n; rewrite {4}def_n {def_n}. have: all prime (primes n) by apply/allP=> p; rewrite mem_primes; case/andP. have:= primes_uniq n; rewrite /primes /divisors; move/prime_decomp: n. elim=> [|[p e] pd] /=; first by split=> // d; rewrite big_nil dvdn1 mem_seq1. rewrite big_cons /=; move: (foldr _ _ pd) => divs. move=> IHpd /andP[npd_p Upd] /andP[pr_p pr_pd]. have lt0p: 0 < p by apply: prime_gt0. have {IHpd Upd}[Udivs Odivs mem_divs] := IHpd Upd pr_pd. have ndivs_p m: p * m \notin divs. suffices: p \notin divs; rewrite !mem_divs. by apply: contra => /dvdnP[n ->]; rewrite mulnCA dvdn_mulr. have ndv_p_1: ~~(p %| 1) by rewrite dvdn1 neq_ltn orbC prime_gt1. rewrite big_seq; elim/big_ind: _ => [//|u v npu npv|[q f] /= pd_qf]. by rewrite Euclid_dvdM //; apply/norP. elim: (f) => // f'; rewrite expnS Euclid_dvdM // orbC negb_or => -> {f'}/=. have pd_q: q \in unzip1 pd by apply/mapP; exists (q, f). by apply: contra npd_p; rewrite dvdn_prime2 // ?(allP pr_pd) // => /eqP->. elim: e => [|e] /=; first by split=> // d; rewrite mul1n. have Tmulp_inj: injective (NatTrec.mul p). by move=> u v /eqP; rewrite !natTrecE eqn_pmul2l // => /eqP. move: (iter e _ _) => divs' [Udivs' Odivs' mem_divs']; split=> [||d]. - rewrite merge_uniq cat_uniq map_inj_uniq // Udivs Udivs' andbT /=. apply/hasP=> [[d dv_d /mapP[d' _ def_d]]]. by case/idPn: dv_d; rewrite def_d natTrecE. - rewrite (merge_sorted leq_total) //; case: (divs') Odivs' => //= d ds. rewrite (@map_path _ _ _ _ leq xpred0) ?has_pred0 // => u v _. by rewrite !natTrecE leq_pmul2l. rewrite mem_merge mem_cat; case dv_d_p: (p %| d). case/dvdnP: dv_d_p => d' ->{d}; rewrite mulnC (negbTE (ndivs_p d')) orbF. rewrite expnS -mulnA dvdn_pmul2l // -mem_divs'. by rewrite -(mem_map Tmulp_inj divs') natTrecE. case pdiv_d: (_ \in _). by case/mapP: pdiv_d dv_d_p => d' _ ->; rewrite natTrecE dvdn_mulr. rewrite mem_divs Gauss_dvdr // coprime_sym. by rewrite coprimeXl ?prime_coprime ?dv_d_p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)