proposition: Lemma Fadjoin_seq_idP (F0 : fieldType) (L : fieldExtType F0) (K : {subfield L}) (xs : seq L) : reflect (<<K & xs>>%VS = K) (all (mem K) xs).
proof: Proof. apply: (iffP idP) => [|<-]; last by apply/allP => x ?; apply: seqv_sub_adjoin. elim: xs => /= [|x xs ih]; first by rewrite Fadjoin_nil. by case/andP=> xK {}/ih ih; rewrite adjoin_cons (Fadjoin_idP _). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)