proposition: Lemma big_cat_nat : forall n m p (P : pred nat) F, m <= n -> n <= p -> \big[*%M/1]_(m <= i < p | P i) F i === (\big[*%M/1]_(m <= i < n | P i) F i) * (\big[*%M/1]_(n <= i < p | P i) F i).
proof: Proof. move=> n m p F P le_mn le_np; rewrite <- big_cat. rewrite -{2}(subnKC le_mn) -iota_add -subn_sub subnKC; [reflexivity|apply leq_sub2]=> //. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops