proposition: Lemma biglcmn_sup (I : finType) i0 (P : pred I) F m : P i0 -> m %| F i0 -> m %| \big[lcmn/1%N]_(i | P i) F i.
proof: Proof. by move=> Pi0 m_Fi0; rewrite (dvdn_trans m_Fi0) // (bigD1 i0) ?dvdn_lcml. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)