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