proposition: Lemma primes_prime p : prime p -> primes p = [::p].
proof: Proof. move=> pr_p; apply: (irr_sorted_eq ltn_trans ltnn) => // [|q]. exact: sorted_primes. rewrite mem_seq1 mem_primes prime_gt0 //=. by apply/andP/idP=> [[pr_q q_p] | /eqP-> //]; rewrite -dvdn_prime2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)