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