proposition: Lemma pi_of_dvd m n : m %| n -> n > 0 -> {subset \pi(m) <= \pi(n)}.
proof: Proof. move=> m_dv_n n_gt0 p; rewrite !mem_primes n_gt0 => /and3P[-> _ p_dv_m]. exact: dvdn_trans p_dv_m m_dv_n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)