proposition: Lemma big_split_ord m n (P : pred 'I_(m + n)) F : \big[*%M/1]_(i | P i) F i = (\big[*%M/1]_(i | P (lshift n i)) F (lshift n i)) * (\big[*%M/1]_(i | P (rshift m i)) F (rshift m i)).
proof: Proof. rewrite -(big_map _ _ (lshift n) _ P F) -(big_map _ _ (@rshift m _) _ P F). rewrite -big_cat; congr bigop; apply: (inj_map val_inj). rewrite map_cat -!map_comp (map_comp (addn m)) /=. by rewrite ![index_enum _]unlock unlock !val_ord_enum -iotaDl addn0 iotaD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)