proposition: Lemma big_prodv_seqP (I : eqType) (r : seq I) (P : {pred I}) (K : fieldType) (aT : falgType K) (U : {vspace aT}) (V : I -> {vspace aT}) (W : {vspace aT}) : uniq r -> reflect (forall u (v : I -> aT), u \in U -> (forall i, P i -> v i \in V i) -> \big[*%R/u]_(i <- r | P i) v i \in W) (\big[@prodv _ _/U]_(i <- r | P i) V i <= W)%VS.
proof: Proof. elim/last_ind: r => [|r i IHr] //= in U W * => [_|]. apply: (iffP idP) => [+ v u uP vP|]; rewrite !big_nil; first by move/subvP->. move=> WP; apply/subvP => u /(WP _ (fun=> 0)); rewrite big_nil; apply. by move=> i; rewrite mem0v. rewrite rcons_uniq => /andP[iNr r_uniq]. apply: (iffP idP) => [+ u v uU vV|WP]; rewrite !big_rcons_idx. by move=> /IHr; apply => //; case: ifP => Pi//; rewrite memv_mul// vV. case: ifP => Pi; last first. by apply/IHr => // u v uU vV; have := WP _ _ uU vV; rewrite big_rcons_idx Pi. apply/IHr => //w v /memv_mulP[n [vs [us [/allP/= vsP /allP/= usP ->]]]] vV. rewrite -big_change_idx/= mulr_sumr rpred_sum// => j _; rewrite big_change_idx. have := WP (tnth us j) (fun k : I => if k == i then tnth vs j else v k). rewrite big_rcons_idx Pi eqxx big_seq_cond. under eq_bigr => k /andP[kr] do [rewrite ifN; last by apply: contraNneq iNr => <-]. rewrite -big_seq_cond; apply; first by rewrite usP ?mem_tnth. by move=> k Pk; case: eqP => [->|]; rewrite ?vV ?vsP ?mem_tnth. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)