proposition: Lemma big_if I r (P Q : pred I) F G : \big[*%M/1]_(i <- r | P i) (if Q i then F i else G i) = \big[*%M/1]_(i <- r | P i && Q i) F i * \big[*%M/1]_(i <- r | P i && ~~ Q i) G i.
proof: Proof. rewrite (bigID Q); congr (_ * _); apply: eq_bigr => i /andP[_]. by move=> ->. by move=> /negPf ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)