proposition: Lemma Rreal_closed_axiom : Num.real_closed_axiom [the numDomainType of R : Type].
proof: Proof. move=> p a b; rewrite !le_eqVlt. case Hpa: ((p.[a])%R == 0%R). by move=> ? _ ; exists a=> //; rewrite lexx le_eqVlt. case Hpb: ((p.[b])%R == 0%R). by move=> ? _; exists b=> //; rewrite lexx le_eqVlt andbT. case Hab: (a == b). by move=> _; rewrite (eqP Hab) eq_sym Hpb (ltNge 0) /=; case/andP=> /ltW ->. rewrite eq_sym Hpb /=; clear=> /RltbP Hab /andP [] /RltbP Hpa /RltbP Hpb. suff Hcp: continuity (fun x => (p.[x])%R). have [z [[Hza Hzb] /eqP Hz2]]:= IVT _ a b Hcp Hab Hpa Hpb. by exists z=> //; apply/andP; split; apply/RlebP. rewrite -[p]coefK poly_def. set f := fun _ => _. have Hf: (fun (x : R) => \sum_(i < size p) (p`_i * x^+i))%R =1 f. move=> x; rewrite /f horner_sum. by apply: eq_bigr=> i _; rewrite hornerZ hornerXn. apply: (continuity_eq Hf); apply: continuity_sum=> i _. apply:continuity_scal; apply: continuity_exp=> x esp Hesp. by exists esp; split=> // y []. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun Zwf Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def Rtrigo1 Reals mathcomp(all_ssreflect ssralg poly mxpoly ssrnum) HB(structures)