fact: Definition real_closed_axiom : Prop := forall (p : {poly R}) (a b : R), a <= b -> p.[a] <= 0 <= p.[b] -> exists2 x, a <= x <= b & root p x.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)