proposition: Lemma conjL_K : {mono conjL : x / x \in K}.
proof: Proof. suff rpJ : {homo conjL : x / x \in K}. by move=> x; apply/idP/idP => /rpJ//; rewrite conjLK. move=> x; rewrite K_eq => xK. have : conjL x \in (linfun conjL @: <<1 & rp>>)%VS. by apply/memv_imgP; exists x => //; rewrite lfunE. rewrite aimg_adjoin_seq aimg1/= (@eq_adjoin _ _ _ _ rp)// => y. apply/mapP/idP => [[z zrp->]|yrp]; first by rewrite lfunE conjL_rp. by exists (conjL y); rewrite ?conjL_rp//= !lfunE [RHS]conjLK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf) Abel(various classic_ext map_gal algR) Abel(char0 cyclotomic_ext real_closed_ext)