proposition: Lemma count_roots_ex : count [predC Creal] example_roots = 2%N.
proof: Proof. rewrite -!sum1_count; pose pR : {poly algR} := poly_example ^^ ratr. have pR0 : pR != 0 by rewrite map_poly_eq0. suff cR : (\sum_(j <- example_roots | j \is Num.real) 1)%N = 3%N. have := size_example_roots; rewrite -sum1_size (bigID (mem Num.real))/=. by rewrite cR => -[->]. rewrite -big_filter (perm_big (map algRval (rootsR pR))); last first. rewrite uniq_perm ?filter_uniq ?example_roots_uniq//. by rewrite (map_inj_uniq (fmorph_inj _)) uniq_roots. move=> x; rewrite mem_filter -root_prod_XsubC -ratr_example_poly. rewrite -(eq_map_poly (fmorph_eq_rat (algRval \o ratr)))/=. rewrite map_poly_comp/=. apply/andP/mapP => [[xR xroot]|[y + ->]]. exists (in_algR xR); rewrite // mem_rootsR// -topredE/=. by rewrite -(mapf_root algRval)/=. rewrite mem_rootsR// -[y \in _]topredE/=. by split; [apply/algRvalP|rewrite mapf_root]. apply/eqP; rewrite sum1_size size_map eqn_leq. rewrite (leq_trans (size_root_leSderiv _))//=; last first. by rewrite deriv_map rootsR_deriv_poly_example. have pRE x : Num.sg pR.[x%:~R] = locked ratr (Num.sg poly_example.[x%:~R]). by rewrite -lock ratr_sg -horner_map/= ratr_int. have pN2 : Num.sg pR.[(- 2%:Z)%:~R] = - 1 by rewrite pRE !pesimp -lock rmorphN1. have pN1 : Num.sg pR.[(- 1%:Z)%:~R] = 1 by rewrite pRE !pesimp -lock rmorph1. have p1 : Num.sg pR.[1%:~R] = - 1 by rewrite pRE !pesimp -lock rmorphN1. have p2 : Num.sg pR.[2%:~R] = 1 by rewrite pRE !pesimp -lock rmorph1. have simp := (pN2, pN1, p1, p2, mulN1r, mulrN1). have [||x0 /andP[_ x0N1] rx0] := @ivt_sign _ pR (- 2%:R) (- 1); rewrite ?simp//. by rewrite -subr_ge0 opprK addKr ler01. have [||x1 /andP[x10 x11] rx1] := @ivt_sign _ pR (-1) 1; rewrite ?simp//. by rewrite -subr_ge0 opprK addr_ge0 ?ler01. have [||x2 /andP[/= x21 _] rx2] := @ivt_sign _ pR 1 2%:R; rewrite ?simp//. by rewrite -subr_ge0 addrK ler01. have: sorted <%R [:: x0; x1; x2] by rewrite /= (lt_trans x0N1) ?(lt_trans x11). rewrite lt_sorted_uniq_le => /andP[uniqx012 _]. apply: (@uniq_leq_size _ [:: x0; x1; x2]) => //. by move=> x; rewrite !inE => /or3P[]/eqP->/=; rewrite mem_rootsR. 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)