proposition: Lemma eq_primes m n : (primes m =i primes n) <-> (primes m = primes n).
proof: Proof. split=> [eqpr| -> //]. by apply: (irr_sorted_eq ltn_trans ltnn); rewrite ?sorted_primes. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)