proposition: Lemma Bernstein_inv2 : forall n (H:S n <= S n), Bernstein H[=]_X_[*](Bernstein (le_S_n _ _ H)).
proof: Proof. intros n H. simpl (Bernstein H). destruct (le_lt_eq_dec _ _ H). exfalso; lia. replace (proj1 (Nat.lt_succ_r n n) H) with (le_S_n n n H) by apply le_irrelevent. 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)