fact: Fixpoint BernsteinBasisTimesXH (n i:nat) (v:Vector.t R i) : i <= n -> Vector.t R (S i) := match v in Vector.t _ i return i <= n -> Vector.t R (S i) with | Vector.nil => fun _ => Vector.cons [0] _ Vector.nil | Vector.cons a i' v' => match n as n return S i' <= n -> Vector.t R (S (S i')) with | O => fun p => False_rect _ (Nat.nle_succ_0 _ p) | S n' => fun p => Vector.cons (eta(Qred (i#P_of_succ_nat n'))[*]a) _ (BernsteinBasisTimesXH v' (Nat.lt_le_incl _ _ p)) 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)