proposition: Lemma evalBernsteinCoefficents : forall p, (let (n,b) := BernsteinCoefficents p in evalBernsteinBasis b)[=]p.
proof: Proof. induction p. reflexivity. simpl. destruct (BernsteinCoefficents p). rewrite -> evalBernsteinBasisPlus. rewrite -> evalBernsteinBasisConst. rewrite -> evalBernsteinBasisTimesX. rewrite -> IHp. rewrite -> poly_linear. ring. Qed.
imports: CoRN.algebra.CPolynomials CoRN.algebra.CSums CoRN.tactics.Rational CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.algebra.CRing_Homomorphisms Coq(Lia)