proposition: Lemma big_split_ord : forall 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. move=> m n P F. rewrite <- (big_map (lshift n) _ P F), <- (big_map (@rshift m _) _ P F), <- big_cat. apply congr_big;move=> *;try reflexivity. by apply: (inj_map (@val_inj _ _ _)); rewrite /index_enum -!enumT val_enum_ord map_cat -map_comp val_enum_ord -map_comp (map_comp (addn m)) val_enum_ord -iota_addl addn0 iota_add. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops