proposition: Lemma factorisationdeg3 : forall z1 z2 z3:C, forall z:C, (z-z1)*(z-z2)*(z-z3)=Cpow z 3+(-(z1+z2+z3))*Cpow z 2+(z1*z2+z2*z3+z3*z1)*z+(-(z1*z2*z3)).
proof: Proof. intros. unfold Cpow. field. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra