proposition: Lemma big_sumType : forall (I1 I2 : finType) (P : pred (I1 + I2)) F, \big[*%M/1]_(i | P i) F i === (\big[*%M/1]_(i | P (inl _ i)) F (inl _ i)) * (\big[*%M/1]_(i | P (inr _ i)) F (inr _ i)).
proof: Proof. move=> I1 I2 P F. rewrite /index_enum [@Finite.enum _]unlock /= /sum_enum; rewrite -> big_cat. rewrite -> (big_map _ (Finite.enum I1)). rewrite -> (big_map _ (Finite.enum I2)). by reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops