proposition: Lemma dvdn_sum d I r (K : pred I) F : (forall i, K i -> d %| F i) -> d %| \sum_(i <- r | K i) F i.
proof: Proof. by move=> dF; elim/big_ind: _ => //; apply: dvdn_add. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)