proposition: Lemma big_cat_idem I r1 r2 (P : pred I) F : \big[op/x]_(i <- r1 ++ r2 | P i) F i = op (\big[op/x]_(i <- r1 | P i) F i) (\big[op/x]_(i <- r2 | P i) F i).
proof: Proof. elim: r1 => [/=|i r1 IHr1]; first by rewrite big_nil opC big_id_idem. by rewrite /= big_cons IHr1 big_cons; case: (P i); rewrite // opA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)