proposition: Lemma gal_permP g i : rp`_(gal_perm g i) = g (rp`_i).
proof: Proof. rewrite /gal_perm; case: sig_eqW => /= s. move=> /(congr1 (((@nth _ 0))^~ i)); rewrite (nth_map 0) ?size_rp// => ->. by rewrite (nth_map i) ?size_enum_ord// (tnth_nth 0)/= nth_ord_enum. 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)