proposition: Lemma big_nat_shift a b c p F: \sum_(c + a <= i < c + b | p i) F i = \sum_(a <= i < b | p (c + i)) F (c + i).
proof: Proof. rewrite /index_iota subnDl unlock; elim: (b - a) {1 3} (a) => // i H d /=. by rewrite -addnS H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)