fact: Fixpoint Bernstein (n i:nat) {struct n}: (i <= n) -> cpoly_cring R := match n return (i <= n) -> cpoly_cring R with O => fun _ => [1] |S n' => match i return (i <= S n') -> cpoly_cring R with O => fun _ => ([1][-]_X_)[*](Bernstein (Nat.le_0_l n')) |S i' => fun p => match (le_lt_eq_dec _ _ p) with | left p' => ([1][-]_X_)[*](Bernstein (proj1 (Nat.lt_succ_r _ _) p'))[+]_X_[*](Bernstein (le_S_n _ _ p)) | right _ => _X_[*](Bernstein (proj1 (Nat.lt_succ_r _ _) p)) end end end.
imports: CoRN.algebra.CPolynomials CoRN.algebra.CSums CoRN.tactics.Rational CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.algebra.CRing_Homomorphisms Coq(Lia)