proposition: Lemma shiftdeg4 : forall u:C, forall a b c d:C, forall z:C, Cpow (z+u) 4+a*Cpow (z+u) 3+b*Cpow (z+u) 2+c*(z+u)+d =Cpow z 4+(a+4*u)*Cpow z 3+(b+3*u*a+6*Cpow u 2)*Cpow z 2 +(c+2*b*u+3*a*Cpow u 2+4*Cpow u 3)*z+(d+c*u+b*Cpow u 2+a*Cpow u 3+Cpow u 4).
proof: Proof. intros. unfold Cpow. rewrite Cval6. rewrite Cval4. rewrite Cval3. rewrite Cval2. field. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra