proposition: Lemma Ztech_derive_sign (n : nat) : isNNegOrNPos (Pol.nth (IP X n.+1) n.+1) = true -> Rcst_sign (fun t => contains (I.convert X) (Xreal t)) (Dn n.+1).
proof: Proof. move=> Hsign. have: Rcst_sign (fun t => contains (I.convert X) (Xreal t)) (fun x => (Dn n.+1 x) / INR (fact n.+1))%R. move: Hsign; set Gamma := Pol.nth _ _. set g := fun x => ((Dn n.+1 x) / INR (fact n.+1))%R. have inGamma : forall x, X >: x -> Gamma >: g x. move => x Hx. rewrite /g -(Poly_nth _ (n:=n.+1)) //. exact: IPoly_nth. rewrite /isNNegOrNPos. case E : I.sign_large =>// _; have := I.sign_large_correct Gamma; rewrite E => Hmain. - left; move=> x Hx. case/(_ _ (inGamma x Hx)): Hmain =>->. exact: Rle_refl. - right; move=> x Hx. now apply (Hmain (Xreal (g x))), inGamma. - left; move=> x Hx. now apply (Hmain (Xreal (g x))), inGamma. case=>[Htop|Htop]; [left|right]; intros x Hx. - apply: Rdiv_pos_compat_rev (Htop x Hx) _. exact: INR_fact_lt_0. - apply: Rdiv_neg_compat_rev (Htop x Hx) _. exact: INR_fact_lt_0. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound