proposition: Lemma big_nseq_cond I n a (P : pred I) F : \big[op/idx]_(i <- nseq n a | P i) F i = if P a then iter n (op (F a)) idx else idx.
proof: Proof. by rewrite unlock; elim: n => /= [|n ->]; case: (P a). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)