proposition: Lemma nrootCC_3_degree : degree n nrootCC_3_poly.
proof: Proof. unfold degree in |- *. split. cut (nth_coeff n nrootCC_3_poly [=] [--]b); intros. apply ap_wdl_unfolded with ( [--]b). apply zero_minus_apart. apply minus_ap_zero. apply inv_resp_ap_zero. exact b_. apply eq_symmetric_unfolded. exact H. unfold nrootCC_3_poly in |- *. Hint Resolve nrCC3_a2: algebra. apply eq_transitive_unfolded with (Im (nth_coeff n nrCC3_poly')). apply nrCC3_a2. Hint Resolve nrCC3_a9: algebra. apply eq_transitive_unfolded with (Im (a[+I*][--]b)). apply Im_wd. exact nrCC3_a9. apply eq_reflexive_unfolded. cut (forall (p : cpoly CC) (n : nat), degree_le n p -> degree_le n (Im_poly p)); intros. unfold nrootCC_3_poly in |- *. apply H. exact nrCC3_a8. unfold degree_le in |- *. unfold degree_le in H. intros. apply eq_transitive_unfolded with (Im (nth_coeff m p)). apply nrCC3_a2. apply eq_transitive_unfolded with (Im ([0]:CC)). apply Im_wd. apply H. exact H0. apply eq_reflexive_unfolded. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing