proposition: Lemma galJ_tperm : gal_perm galJ = tperm i0 i1.
proof: Proof. apply/permP => i; apply/val_inj. apply: (uniqP 0 rp_uniq); rewrite ?inE ?size_rp ?ltn_ord//=. rewrite gal_permP /galJ/= galK ?rpK//= ?lfunE ?[LHS]conj_nth_rp//. by apply/subvP => /= _/memv_imgP[x Ex ->]; rewrite lfunE conjL_K. 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)