proposition: Lemma nth_rp_real i : (iota rp`_i \is Num.real) = (i > 1)%N.
proof: Proof. rewrite nth_cat size_filter count_rp'; case: ltnP => // iP; [apply/negbTE|]. apply: (allP (filter_all [predC (mem Creal) \o iota] _)) _ (mem_nth 0 _). by rewrite size_filter count_rp'. have [i_big|i_small] := leqP (size [seq x <- rp' | iota x \is Creal]) (i - 2). by rewrite nth_default// rmorph0 rpred0. exact: (allP (filter_all (mem Creal \o iota) _)) _ (mem_nth 0 _). 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)