proposition: Lemma rext_trans r (F E K : {subfield L}) : r.-ext E F -> r.-ext F K -> r.-ext E K.
proof: Proof. move=> [[/= n1 e1 pw1] Ee FE] [[/= n2 e2 pw2] Fe KE]. exists (ExtData [tuple of e1 ++ e2] [tuple of pw1 ++ pw2]) => /=; last first. by rewrite adjoin_cat FE. apply/towerP => /= i; case: (unsplitP i) => [j eq_ij|k eq_i_n1Dk]. - rewrite eq_ij !tnth_lshift takel_cat /=; last first. by rewrite size_tuple ltnW. by move/forallP/(_ j): Ee. - rewrite eq_i_n1Dk take_cat size_tuple ltnNge leq_addr /= addKn. by rewrite adjoin_cat FE !tnth_rshift; move/forallP/(_ k): Fe. 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)