proposition: Lemma tower_sub r1 r2 n E (e : n.-tuple L) (pw : n.-tuple nat) : (forall U x n, r1 U x n -> r2 U x n) -> r1.-tower E e pw -> r2.-tower E e pw.
proof: Proof. by move=> sub_r /forallP /= h; apply/forallP=> /= i; apply/sub_r/h. 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)