fact: Fixpoint subeval (f : algterm F) : seq algC := algT_eval f :: match f with | UnOp _ f1 => subeval f1 | BinOp _ f1 f2 => subeval f1 ++ subeval f2 | _ => [::] end.
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)