fact: Definition closed_field_axiom (R : ringType) := forall n (P : nat -> R), n > 0 -> exists x : R, x ^+ n = \sum_(i < n) P i * (x ^+ i).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)