proposition: Lemma filter_pi_of n m : n < m -> filter \pi(n) (index_iota 0 m) = primes n.
proof: Proof. move=> lt_n_m; have ltnT := ltn_trans; apply: (irr_sorted_eq ltnT ltnn). - by rewrite sorted_filter // iota_ltn_sorted. - exact: sorted_primes. move=> p; rewrite mem_filter mem_index_iota /= mem_primes; case: and3P => //. by case=> _ n_gt0 dv_p_n; apply: leq_ltn_trans lt_n_m; apply: dvdn_leq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)