proposition: Lemma big_dvdr (I : finType) (d : R) (F : I -> R) (P : pred I) : (forall i, d %| F i) -> d %| \sum_(i : I | P i) (F i).
proof: Proof. move=> H; elim: (index_enum I)=> [|a l IHl]. by rewrite big_nil dvdr0. rewrite big_cons; case: (P a). by rewrite dvdr_addl; [apply: H | apply: IHl]. exact: IHl. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete