proposition: Lemma eq_adjoin (K : fieldType) (aT : falgType K) (U : {vspace aT}) (rs1 rs2 : seq aT) : rs1 =i rs2 -> <<U & rs1>>%VS = <<U & rs2>>%VS.
proof: Proof. by move=> rs12; apply/eqP; rewrite eqEsubv !adjoin_seqSr// => x; rewrite rs12. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)