proposition: Lemma RaiseDegreeA : forall n i (H:i<=n), (nring (S n))[*]_X_[*]Bernstein H[=](nring (S i))[*]Bernstein (le_n_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). rstepl (nring (S n)[*]_X_[*]Bernstein H[+]_X_[*]Bernstein H). destruct i as [|i]. simpl (Bernstein H) at 1. rstepl (([1][-]_X_)[*](nring (S n)[*]_X_[*]Bernstein (Nat.le_0_l n))[+] _X_[*]Bernstein H). rewrite -> IHn. rstepl ((([1][-]_X_)[*]Bernstein (le_n_S _ _ (Nat.le_0_l n))[+]_X_[*]Bernstein H)). rstepr (Bernstein (le_n_S 0 (S n) H)). set (le_n_S 0 n (Nat.le_0_l n)). rewrite (Bernstein_inv1 l). rewrite (le_irrelevent _ _ (proj1 (Nat.lt_succ_r 1 (S n)) (proj1 (Nat.succ_lt_mono 0 (S n)) l)) l). rewrite (le_irrelevent _ _ H (le_S_n 0 (S n) (le_n_S 0 (S n) H))). reflexivity. simpl (Bernstein H) at 1. destruct (le_lt_eq_dec _ _ H). rstepl (([1][-]_X_)[*](nring (S n)[*]_X_[*]Bernstein (proj1 (Nat.lt_succ_r (S i) n) l))[+] _X_[*](nring (S n)[*]_X_[*]Bernstein (le_S_n i n H))[+] _X_[*]Bernstein H). do 2 rewrite -> IHn. change (nring (S (S i)):cpoly_cring R) with (nring (S i)[+][1]:cpoly_cring R). set (l0:= (le_n_S (S i) n (proj1 (Nat.lt_succ_r (S i) n) l))). replace (le_n_S i n (le_S_n i n H)) with H by apply le_irrelevent. rstepl ((nring (S i)[+][1])[*](([1][-]_X_)[*]Bernstein l0[+]_X_[*]Bernstein H)). rewrite (Bernstein_inv1 l). replace (proj1 (Nat.lt_succ_r (S (S i)) (S n)) (proj1 (Nat.succ_lt_mono (S i) (S n)) l)) with l0 by apply le_irrelevent. replace (le_S_n (S i) (S n) (le_n_S (S i) (S n) H)) with H by apply le_irrelevent. reflexivity. rstepl (_X_[*](nring (S n)[*]_X_[*]Bernstein (proj1 (Nat.lt_succ_r _ _) H))[+] _X_[*]Bernstein H). rewrite IHn. replace (le_n_S i n (proj1 (Nat.lt_succ_r i n) H)) with H by apply le_irrelevent. revert H. inversion_clear e. intros H. rewrite -> (Bernstein_inv2 (le_n_S _ _ H)). replace (le_S_n (S n) (S n) (le_n_S (S n) (S n) H)) with H by apply le_irrelevent. change (nring (S (S n)):cpoly_cring R) with (nring (S n)[+][1]:cpoly_cring R). 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)