proposition: Lemma eq_piP m n : \pi(m) =i \pi(n) <-> \pi(m) = \pi(n).
proof: Proof. rewrite /pi_of; have eqs := irr_sorted_eq ltn_trans ltnn. by split=> [|-> //] /(eqs _ _ (sorted_primes m) (sorted_primes n)) ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)