proposition: Lemma RaiseDegree : forall n i (H: i<=n), (nring (S n))[*]Bernstein H[=](nring (S n - i))[*]Bernstein (le_S _ _ H)[+](nring (S i))[*]Bernstein (le_n_S _ _ H).
proof: Proof. intros n i H. rstepl ((nring (S n))[*]([1][-]_X_)[*]Bernstein H[+](nring (S n))[*]_X_[*]Bernstein H). rewrite RaiseDegreeA, RaiseDegreeB. reflexivity. Qed.
imports: CoRN.algebra.CPolynomials CoRN.algebra.CSums CoRN.tactics.Rational CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.algebra.CRing_Homomorphisms Coq(Lia)