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