proposition: Lemma adjoin_cat (K : fieldType) (aT : falgType K) (V : {vspace aT}) (rs1 rs2 : seq aT) : <<V & rs1 ++ rs2>>%VS = <<<<V & rs1>> & rs2>>%VS.
proof: Proof. elim: rs1 => /= [|r rs1 ih] in V *. - by rewrite adjoin_nil agenv_add_id. - by rewrite !adjoin_cons ih. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)