proposition: Lemma sorted_primes n : sorted ltn (primes n).
proof: Proof. by case: (posnP n) => [-> // | /prime_decomp_correct[_ _]]; apply: path_sorted. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)