proposition: Lemma rootsR_deriv_poly_example : rootsR (poly_example^`() ^^ ratr) = [:: - alpha; alpha].
proof: Proof. apply: lt_sorted_eq; rewrite ?sorted_roots//. by rewrite /= andbT -subr_gt0 opprK ?addr_gt0 ?alpha_gt0. move=> x; rewrite mem_rootsR ?map_poly_eq0// !inE -topredE/= orbC. rewrite deriv_poly_example /root. rewrite rmorphB /= linearZ map_polyC/= map_polyXn !pesimp. rewrite -[5%:R]sqr_sqrtr ?ler0n// (exprM _ 2 2) -exprMn (natrX _ 2 2) subr_sqr. rewrite mulf_eq0 [_ + 2%:R == 0]gt_eqF ?orbF; last first. by rewrite ltr_spaddr ?ltr0n// mulr_ge0 ?sqrtr_ge0// exprn_even_ge0. have sqrt5N0 : Num.sqrt (5%:R : algR) != 0 by rewrite gt_eqF// sqrtr_gt0 ?ltr0n. rewrite subr_eq0 (can2_eq (mulKf _) (mulVKf _))// mulrC -subr_eq0. rewrite -[X in _ - X]sqr_sqrtr; last first. by rewrite mulr_ge0 ?invr_ge0 ?sqrtr_ge0 ?ler0n. by rewrite subr_sqr mulf_eq0 subr_eq0 addr_eq0. 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)