proposition: Lemma eq_big_op I r (P : pred I) F (K_F : forall i, P i -> K (F i)) : \big[op/idx]_(i <- r | P i) F i = \big[op'/idx]_(i <- r | P i) F i.
proof: Proof. by elim/(big_load K): _; elim/big_rec2: _ => // i _ y Pi [Ky <-]; auto. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)