proposition: Lemma upper_Rneg_over (c x0 : R) (nm1 : nat) (n := nm1.+1) : dom x0 -> Rneg_over dom (Dn n.+1) -> forall x : R, (x0 <= x)%R -> dom x -> intvl x x0 c \/ intvl x0 x c -> (Dn n.+1 c / INR (fact n) * (x - x0) ^ n <= 0)%R.
proof: Proof. move=> Hx0 Hsign x Hx Dx [Hc|Hc]. have ->: x = x0. by move: Hx Hc; rewrite /intvl; lra. by rewrite Rminus_diag_eq // pow_ne_zero // Rmult_0_r; auto with real. apply: Rmult_le_neg_pos. apply: Rdiv_neg_compat. apply: Hsign. exact: Hdom Hc. exact: INR_fact_lt_0. apply: pow_le. now apply Rle_0_minus. 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