proposition: Lemma rext_r r n (U : {subfield L}) x : r U x n -> r.-ext U << U; x >>%VS.
proof: Proof. move=> rUxn; exists (ExtData [tuple x] [tuple n]); last by rewrite adjoin_seq1. by apply/towerP => /= i; rewrite ord1/= !tnth0 Fadjoin_nil. 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)