proposition: Lemma Bernstein_ind : forall n i (H:i<=n) (P : nat -> nat -> cpoly_cring R -> Prop), P 0 0 [1] -> (forall n p, P n 0 p -> P (S n) 0 (([1][-]_X_)[*]p)) -> (forall n p, P n n p -> P (S n) (S n) (_X_[*]p)) -> (forall i n p q, (i < n) -> P n i p -> P n (S i) q -> P (S n) (S i) (([1][-]_X_)[*]q[+]_X_[*]p)) -> P n i (Bernstein H).
proof: Proof. intros n i H P H0 H1 H2 H3. revert n i H. induction n; intros [|i] H. apply H0. exfalso; auto with *. apply H1. apply IHn. simpl. destruct (le_lt_eq_dec (S i) (S n)). apply H3; auto with *. inversion e. revert H. rewrite H5. intros H. apply H2. 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)