proposition: Lemma big_catl r1 r2 (P : pred I) F : ~~ has P r2 -> \big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/idx]_(i <- r1 | P i) F i.
proof: Proof. by rewrite big_cat_nested => /big_hasC->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)