proposition: Lemma big_cat_nat_idem n m p (P : pred nat) F : m <= n -> n <= p -> \big[op/x]_(m <= i < p | P i) F i = op (\big[op/x]_(m <= i < n | P i) F i) (\big[op/x]_(n <= i < p | P i) F i).
proof: Proof. move=> le_mn le_np; rewrite -big_cat_idem -{2}(subnKC le_mn) -iotaD subnDA. by rewrite subnKC // leq_sub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)