proposition: Lemma big_rec3 I r (P : pred I) F1 F2 F3 (K_F : forall i y1 y2 y3, P i -> K y1 y2 y3 -> K (op1 (F1 i) y1) (op2 (F2 i) y2) (op3 (F3 i) y3)) : K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i) (\big[op3/id3]_(i <- r | P i) F3 i).
proof: Proof. by rewrite unlock; elim: r => //= i r; case: ifP => //; apply: K_F. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)