Variable R : COrdField.
Lemma Cbigger : forall x y : R, {z : R | x [<=] z | y [<=] z}.
Lemma Ccpoly_big : forall (p : R[x]) n, 0 < n ->
monic n p -> forall Y, {X : R | forall x, X [<=] x -> Y [<=] p ! x}.
Lemma cpoly_pos : forall (p : R[x]) n, 0 < n -> monic n p -> {x : R | 0 [<=] p ! x}.
Lemma Ccpoly_pos' : forall (p : R[x]) a n, 0 < n -> monic n p -> {x : R | a [<] x | 0 [<=] p ! x}.
End CPoly_Big.
Section Flip_Poly.
Variable R : CRing.
Fixpoint flip (p : R[x]) : R[x] :=
match p with
| cpoly_zero => cpoly_zero _
| cpoly_linear c q => cpoly_inv _ (cpoly_linear _ c (flip q))
end.
Lemma flip_poly : forall (p : R[x]) x, (flip p) ! x [=] [--]p ! ( [--]x).
Lemma flip_coefficient : forall (p : R[x]) i,
nth_coeff i (flip p) [=] [--] ( [--]1[^]i) [*]nth_coeff i p.
Lemma flip_odd : forall (p : R[x]) n, odd n -> monic n p -> monic n (flip p).
End Flip_Poly.
Section OddPoly_Signs.
Variable R : COrdField.
Lemma oddpoly_pos : forall (p : R[x]) n, odd n -> monic n p -> {x : R | 0 [<=] p ! x}.
Lemma oddpoly_pos' : forall (p : R[x]) a n,
odd n -> monic n p -> {x : R | a [<] x | 0 [<=] p ! x}.
Lemma oddpoly_neg : forall (p : R[x]) n, odd n -> monic n p -> {x : R | p ! x [<=] 0}.
End OddPoly_Signs.
Section Poly_Norm.
Variable R : CField.
Lemma poly_norm_aux : forall (p : R[x]) n, degree n p -> nth_coeff n p [#] 0.
Definition poly_norm p n H := _C_ (1[/] _[//]poly_norm_aux p n H) [*]p.
Lemma poly_norm_monic : forall p n H, monic n (poly_norm p n H).
Lemma poly_norm_apply : forall p n H x, (poly_norm p n H) ! x [=] 0 -> p ! x [=] 0.
End Poly_Norm.
Section OddPoly_Root.
Lemma oddpoly_root' : forall f n, odd n -> monic n f -> {x : IR | f ! x [=] 0}.
Lemma oddpoly_root : forall f n, odd n -> degree n f -> {x : IR | f ! x [=] 0}.
Lemma realpolyn_oddhaszero : forall f, odd_cpoly _ f -> {x : IR | f ! x [=] 0}.
End OddPoly_Root.