proposition: Lemma widen_partn m pi n : n <= m -> n`_pi = \prod_(0 <= p < m.+1 | p \in pi) p ^ logn p n.
proof: Proof. move=> le_n_m; rewrite big_mkcond /=. rewrite [n`_pi](big_nat_widen _ _ m.+1) // big_mkcond /=. apply: eq_bigr => p _; rewrite ltnS lognE. by case: and3P => [[_ n_gt0 p_dv_n]|]; rewrite ?if_same // andbC dvdn_leq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)