proposition: Lemma modn_summ I r (P : pred I) F d : \sum_(i <- r | P i) F i %% d = \sum_(i <- r | P i) F i %[mod d].
proof: Proof. by apply/eqP; elim/big_rec2: _ => // i m n _; rewrite modnDml eqn_modDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)