proposition: Lemma dvdn_biglcmP (I : finType) (P : pred I) F m : reflect (forall i, P i -> F i %| m) (\big[lcmn/1%N]_(i | P i) F i %| m).
proof: Proof. apply: (iffP idP) => [dvFm i Pi | dvFm]. by rewrite (bigD1 i) // dvdn_lcm in dvFm; case/andP: dvFm. by elim/big_ind: _ => // p q p_m; rewrite dvdn_lcm p_m. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)