proposition: Lemma CnrootIR : {x : IR | [0] [<=] x | x[^]n [=] c}.
proof: Proof. intros. cut (monic n p). intro. elim (Ccpoly_pos' _ p [0] n); auto. intro X. intros H0 H1. cut {x : IR | [0] [<=] x /\ x [<=] X /\ p ! x [=] [0]}. intro H2. elim H2. clear H2. intro. intro H2. elim H2. clear H2. intros H2 H3. elim H3. clear H3. intros. exists x. auto. apply cg_inv_unique_2. astepl (_X_ ! x[^]n[-] (_C_ c) ! x). astepl ((_X_[^]n) ! x[-] (_C_ c) ! x). Step_final (_X_[^]n[-]_C_ c) ! x. apply Civt_poly; auto. apply monic_apzero with n; auto. unfold p in |- *. astepl ((_X_[^]n) ! [0][-] (_C_ c) ! [0]). astepl (_X_ ! [0][^]n[-]c). astepl ([0][^]n[-]c). astepl ([0][-]c). astepl ( [--]c). astepr ( [--]ZeroR). apply inv_resp_leEq. auto. unfold p in |- *. apply monic_minus with 0. apply degree_le_c_. pattern n at 1 in |- *. replace n with (1 * n). apply monic_nexp. apply monic_x_. auto with arith. auto. Qed.
imports: CoRN.reals.OddPolyRootIR