proposition: Lemma conj_rp0 : conjL rp`_i0 = rp`_i1.
proof: Proof. have /(nthP 0)[j jlt /esym rpj_eq]: conjL rp`_i0 \in rp. by rewrite conjL_rp mem_nth ?size_rp. rewrite size_rp in jlt; rewrite rpj_eq; congr nth. have: j != i0. apply: contra_eq_neq rpj_eq => ->. by rewrite -(inj_eq (fmorph_inj iota)) iotaJ -CrealE nth_rp_real. have: (j < 2)%N by rewrite ltnNge -nth_rp_real -rpj_eq iotaJ CrealJ nth_rp_real. by case: j {jlt rpj_eq} => [|[|[]]]. 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)