proposition: Lemma big_ind I r (P : pred I) F (K_F : forall i, P i -> K (F i)) : K (\big[op/idx]_(i <- r | P i) F i).
proof: Proof. by apply: big_rec => // i x /K_F /Kop; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)