proposition: Lemma evalBernsteinBasisTimesX : forall n (v:Vector.t R n), evalBernsteinBasis (BernsteinBasisTimesX v)[=]_X_[*]evalBernsteinBasis v.
proof: Proof. intros n. unfold evalBernsteinBasis, BernsteinBasisTimesX. generalize (Nat.le_refl (S n)) (Nat.le_refl n). generalize n at 1 3 5 7 9 11. intros i. induction i. intros l l0 v. rewrite (V0_eq v). simpl. rewrite <- c_zero. ring. intros l l0 v. destruct n as [|n]. exfalso; auto with *. rewrite (VSn_eq v). simpl. rewrite -> IHi. rewrite -> c_mult. rewrite -> ring_dist_unfolded. apply csbf_wd; try reflexivity. set (A:= (_C_ (eta (Qred (Qmake (Zpos (P_of_succ_nat i)) (P_of_succ_nat n)))))). rstepl (_C_ (Vector.hd v)[*](A[*]Bernstein (le_S_n (S i) (S n) l))). rstepr (_C_ (Vector.hd v)[*](_X_[*]Bernstein (le_S_n i n l0))). apply mult_wdr. unfold A; clear A. assert (Hn : (nring (S n):Q)[#][0]). stepl (S n:Q). simpl. unfold Qap, Qeq. auto with *. symmetry; apply nring_Q. setoid_replace (Qred (P_of_succ_nat i # P_of_succ_nat n)) with (([1][/](nring (S n))[//]Hn)[*](nring (S i))). set (eta':=RHcompose _ _ _ _C_ eta). change (_C_ (eta (([1][/]nring (S n)[//]Hn)[*]nring (S i)))) with ((eta' (([1][/]nring (S n)[//]Hn)[*]nring (S i))):cpoly_cring R). rewrite -> rh_pres_mult. rewrite -> rh_pres_nring. rewrite <- mult_assoc_unfolded. replace (le_S_n (S i) (S n) l) with (le_n_S _ _ (le_S_n i n l0)) by apply le_irrelevent. rewrite <- RaiseDegreeA. rewrite <- (@rh_pres_nring _ _ eta'). rewrite <- mult_assoc_unfolded. rewrite -> mult_assoc_unfolded. rewrite <- rh_pres_mult. setoid_replace (eta' (([1][/]nring (S n)[//]Hn)[*]nring (S n))) with ([1]:cpoly_cring R). ring. rewrite <- (@rh_pres_unit _ _ eta'). apply csf_wd. apply (@div_1 Q_as_CField). rewrite -> Qred_correct. rewrite -> Qmake_Qdiv. change (Zpos (P_of_succ_nat n)) with ((S n):Z). rewrite <- (nring_Q (S n)). change (Zpos (P_of_succ_nat i)) with ((S i):Z). rewrite <- (nring_Q (S i)). change (nring (S i)/nring (S n) == (1/(nring (S n)))*nring (S i))%Q. field. apply Hn. Qed.
imports: CoRN.algebra.CPolynomials CoRN.algebra.CSums CoRN.tactics.Rational CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.algebra.CRing_Homomorphisms Coq(Lia)