proposition: Lemma big_prodv_eq_aspace I (r : seq I) (P : {pred I}) (F : I -> {aspace L}) : (\big[@prodv _ _/1%VS]_(i <- r | P i) F i) = (\big[@prodv_aspace _ _/1%AS]_(i <- r | P i) F i).
proof: Proof. by elim/big_rec2: _ => // i U V _ ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)