proposition: Lemma BernsteinNonNeg : forall x:F, [0] [<=] x -> x [<=] [1] -> forall n i (p:Nat.le i n), [0][<=](Bernstein F p)!x.
proof: Proof. intros x Hx0 Hx1. induction n. intros i p. simpl (Bernstein F p). autorewrite with apply. auto with *. intros [|i] p; simpl (Bernstein F p). autorewrite with apply. auto with *. destruct (le_lt_eq_dec (S i) (S n) p); autorewrite with apply; auto with *. Qed.
imports: CoRN.algebra.CPolynomials CoRN.algebra.CSums CoRN.tactics.Rational CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.algebra.CRing_Homomorphisms Coq(Lia)