proposition: Lemma RaiseDegreeB : forall n i (H:i<=n), (nring (S n))[*]([1][-]_X_)[*]Bernstein H[=](nring (S n - i))[*]Bernstein (le_S _ _ H).
proof: Proof. induction n. intros [|i] H; [|exfalso; lia]. repeat split; ring. intros i H. change (nring (S (S n)):cpoly_cring R) with (nring (S n)[+][1]:cpoly_cring R). set (X0:=([1][-](@cpoly_var R))) in *. rstepl (nring (S n)[*]X0[*]Bernstein H[+]X0[*]Bernstein H). destruct i as [|i]. simpl (Bernstein H) at 1. fold X0. rstepl (X0[*](nring (S n)[*]X0[*]Bernstein (Nat.le_0_l n))[+] X0[*]Bernstein H). rewrite -> IHn. replace (le_S 0 n (Nat.le_0_l n)) with H by apply le_irrelevent. simpl (S n - 0). change (nring (S (S n) - 0):cpoly_cring R) with (nring (S n)[+][1]:cpoly_cring R). rstepl ((nring (S n))[*](X0[*]Bernstein H)[+]X0[*]Bernstein H). change (Bernstein (le_S _ _ H)) with (X0[*]Bernstein (Nat.le_0_l (S n))). replace (Nat.le_0_l (S n)) with H by apply le_irrelevent. ring. simpl (Bernstein H) at 1. destruct (le_lt_eq_dec _ _ H). fold X0. rstepl (X0[*](nring (S n)[*]X0[*]Bernstein (proj1 (Nat.lt_succ_r (S i) n) l))[+] _X_[*](nring (S n)[*]X0[*]Bernstein (le_S_n i n H))[+] X0[*]Bernstein H). do 2 rewrite -> IHn. rewrite (Nat.sub_succ_l i n) by auto with *. rewrite (Nat.sub_succ_l (S i) (S n)) by auto with *. replace (S n - S i) with (n - i) by auto with *. change (nring (S (n - i)):cpoly_cring R) with (nring (n - i)[+][1]:cpoly_cring R). replace (le_S (S i) n (proj1 (Nat.lt_succ_r (S i) n) l)) with H by apply le_irrelevent. set (l0:= (le_S i n (le_S_n i n H))). rstepl ((nring (n - i)[+][1])[*](X0[*]Bernstein H[+]_X_[*]Bernstein l0)). rewrite -> (Bernstein_inv1 H). fold X0. replace (proj1 (Nat.lt_succ_r _ _) (proj1 (Nat.succ_lt_mono _ _) H)) with H by apply le_irrelevent. replace (le_S_n _ _ (le_S (S i) (S n) H)) with l0 by apply le_irrelevent. reflexivity. revert H. inversion e. clear - IHn. intros H. assert (l:(n < (S n))) by auto. rewrite -> (Bernstein_inv1 l). fold X0. rstepl (_X_[*](nring (S n)[*]X0[*]Bernstein (proj1 (Nat.lt_succ_r _ _) H))[+] X0[*]Bernstein H). rewrite -> IHn. replace (S n - n) with 1 by auto with *. replace (S (S n) - S n) with 1 by auto with *. replace (le_S_n n (S n) (le_S (S n) (S n) H)) with (le_S n n (proj1 (Nat.lt_succ_r n n) H)) by apply le_irrelevent. replace (proj1 (Nat.lt_succ_r (S n) (S n)) (proj1 (Nat.succ_lt_mono n (S n)) l)) with H by apply le_irrelevent. ring. Qed.
imports: CoRN.algebra.CPolynomials CoRN.algebra.CSums CoRN.tactics.Rational CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.algebra.CRing_Homomorphisms Coq(Lia)