proposition: Lemma big_tuple_ffun (I J : finType) (F : {ffun I -> J} -> R) (G : R -> J -> V) (jdef : J) (idef : I) : \big[+%M/GRing.zero V]_(j : #|I|.-tuple J) G (F [ffun x => tnth j (enum_rank x)]) (nth jdef j 0) = \big[+%M/GRing.zero V]_(f : {ffun I -> J}) G (F f) (f (nth idef (enum I) 0)).
proof: Proof. rewrite (reindex_onto (fun y => fgraph y) (fun p => [ffun x => tnth p (enum_rank x)])); last first. move=> t _; by apply/eq_from_tnth => i; rewrite tnth_fgraph ffunE enum_valK. apply eq_big. move=> f /=; apply/eqP/ffunP => i; by rewrite ffunE tnth_fgraph enum_rankK. move=> f _. congr (G (F _) _). apply/ffunP => i; by rewrite ffunE tnth_fgraph enum_rankK. have @zero : 'I_#|I| by exists O; apply/card_gt0P; exists idef. transitivity (tnth (fgraph f) zero). apply set_nth_default; by rewrite size_tuple ltn_ord. rewrite tnth_fgraph; congr (f _). by apply enum_val_nth. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext