proposition: Lemma sorted_divisors_ltn n : sorted ltn (divisors n).
proof: Proof. by rewrite ltn_sorted_uniq_leq divisors_uniq sorted_divisors. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)