proposition: Lemma piSg G H : G \subset H -> {subset \pi(gval G) <= \pi(gval H)}.
proof: Proof. move=> sGH p; rewrite !mem_primes !cardG_gt0 => /and3P[-> _ pG]. exact: dvdn_trans (cardSg sGH). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)