proposition: Lemma sub_in_partn pi1 pi2 n : {in \pi(n), {subset pi1 <= pi2}} -> n`_pi1 %| n`_pi2.
proof: Proof. move=> pi12; rewrite ![n`__]big_mkcond /=. apply (big_ind2 (fun m1 m2 => m1 %| m2)) => // [*|p _]; first exact: dvdn_mul. rewrite lognE -mem_primes; case: ifP => pi1p; last exact: dvd1n. by case: ifP => pr_p; [rewrite pi12 | rewrite if_same]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)