proposition: Lemma Binom_solution_proof : forall (b:C) (c:C), forall z:C, Cpow z 2+b*z+c=(z-binom_solution b c 0)*(z-binom_solution b c 1).
proof: Proof. intros. transitivity (Cpow z 2+-(binom_solution b c 0+binom_solution b c 1)*z +(binom_solution b c 0)*(binom_solution b c 1)). unfold binom_solution. unfold Cpow. f_equal. f_equal. f_equal. repeat rewrite Cmult_1_r. assert(forall (f:C) (g:C), (f+g)+(f+g*(-1))=f+f) as aux1. intros. destruct f,g. unfold RtoC,Cmult,Copp,Cplus,fst,snd. f_equal;field. rewrite aux1. rewrite Cval2. field; nneq0. repeat rewrite Cmult_1_r. assert(forall u v :C, (u+v)*(u+v*-1)=u*u-v*v) as diffsq. intros. destruct u,v. unfold RtoC,Cminus,Cmult,Copp,Cplus,fst,snd. f_equal;field. rewrite diffsq. rewrite Csqrt_Cpow2. field; nneq0. unfold Cpow. field. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra