proposition: Lemma evalBernsteinBasisPlus : forall n (v1 v2: Vector.t R n), evalBernsteinBasis (Vbinary (fun (x y:R)=>x[+]y) v1 v2)[=]evalBernsteinBasis v1[+]evalBernsteinBasis v2.
proof: Proof. unfold evalBernsteinBasis. intros n. generalize (Nat.le_refl n). generalize n at 1 3 4 6 7 9 11. intros i. induction i. intros l v1 v2. rewrite (V0_eq v1), (V0_eq v2). ring. intros l v1 v2. destruct n as [|n]. exfalso; auto with *. rewrite (VSn_eq v1), (VSn_eq v2). simpl. rewrite IHi. rewrite -> c_plus. 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)