proposition: Lemma big_nat_cond_eq a b p p' F : (forall i, a <= i < b -> (p i = p' i)) -> \sum_(a <= i < b | p i) F i = \sum_(a <= i < b | p' i) F i.
proof: Proof. rewrite big_nat_cond [in RHS] big_nat_cond => H; apply: eq_bigl => i. by apply: (andb_id2l (H i)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)