proposition: Lemma Civt_poly : forall f : cpoly_cring IR, f [#] [0] -> forall a b, a [<] b -> f ! a [<=] [0] -> [0] [<=] f ! b -> {x : IR | a [<=] x /\ x [<=] b /\ f ! x [=] [0]}.
proof: Proof. intros. cut ({x : IR | a [<=] x /\ x [<=] b /\ cpoly_csetoid_op _ f x [=] [0]}). intro. auto. apply Civt_op; auto. apply cpoly_op_contin. intros. change {c : IR | a0 [<=] c /\ c [<=] b0 | f ! c [#] [0]} in |- *. apply Cpoly_apzero_interval. auto. auto. Qed.
imports: CoRN.reals.CPoly_Contin