proposition: Lemma Bernstein_inv1 : forall n i (H:i < n) (H0:S i <= S n), Bernstein H0[=]([1][-]_X_)[*](Bernstein (proj1 (Nat.lt_succ_r _ _) (proj1 (Nat.succ_lt_mono _ _) H)))[+]_X_[*](Bernstein (le_S_n _ _ H0)).
proof: Proof. intros n i H H0. simpl (Bernstein H0). destruct (le_lt_eq_dec _ _ H0). replace (proj1 (Nat.lt_succ_r (S i) n) l) with (proj1 (Nat.lt_succ_r _ _) (proj1 (Nat.succ_lt_mono _ _) H)) by apply le_irrelevent. reflexivity. exfalso; lia. Qed.
imports: CoRN.algebra.CPolynomials CoRN.algebra.CSums CoRN.tactics.Rational CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.algebra.CRing_Homomorphisms Coq(Lia)