proposition: Lemma evalBernsteinBasisConst : forall n c, evalBernsteinBasis (Vector.const c (S n))[=]_C_ c.
proof: Proof. intros n c. stepr (evalBernsteinBasis (Vector.const c (S n))[+]_C_ c[*]Sum (S n) n (part_tot_nat_fun _ _ (fun (i : nat) (H : i < S n) => Bernstein (proj1 (Nat.lt_succ_r i n) H)))). rewrite -> Sum_empty by auto with *. ring. unfold evalBernsteinBasis. generalize (Nat.le_refl (S n)). generalize (S n) at 1 4 5 6. intros i l. induction i. rstepr (_C_ c[*][1]). rewrite <- (partitionOfUnity n). rewrite -> Sumx_to_Sum; auto with *. intros i j Hij. rewrite Hij. intros H H'. replace (proj1 (Nat.lt_succ_r j n) H) with (proj1 (Nat.lt_succ_r j n) H') by apply le_irrelevent. reflexivity. rstepl (evalBernsteinBasisH (Vector.const c i) (Nat.lt_le_incl i (S n) l)[+] _C_ c[*](Bernstein (le_S_n i n l)[+] Sum (S i) n (part_tot_nat_fun (cpoly_cring R) (S n) (fun (i0 : nat) (H : i0 < S n) => Bernstein (proj1 (Nat.lt_succ_r i0 n) H))))). replace (Bernstein (le_S_n _ _ l)) with (part_tot_nat_fun (cpoly_cring R) (S n) (fun (i0 : nat) (H : i0 < S n) => Bernstein (proj1 (Nat.lt_succ_r i0 n) H)) i). rewrite <- Sum_first. apply IHi. clear - i. unfold part_tot_nat_fun. destruct (le_lt_dec (S n) i). exfalso; auto with *. simpl. replace (proj1 (Nat.lt_succ_r _ _) l0) with (le_S_n _ _ l) by apply le_irrelevent. reflexivity. Qed.
imports: CoRN.algebra.CPolynomials CoRN.algebra.CSums CoRN.tactics.Rational CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.algebra.CRing_Homomorphisms Coq(Lia)