proposition: Lemma ZOdd_pow_le (r : R) (n : nat) : Z.Odd (Z_of_nat n) -> (r <= 0 -> r ^ n <= 0)%R.
proof: Proof. move=> [k Hk] Hneg. rewrite pow_Rabs_sign; case: Rle_bool_spec =>[Hr|Hr]. have->: r = R0 by psatzl R. rewrite Rabs_R0 pow_ne_zero ?Rmult_0_r; first by auto with real. by lia. rewrite Hk. apply: Rmult_le_neg_pos; last by apply: pow_le; exact: Rabs_pos. rewrite powerRZ_add; discrR. apply: Rmult_le_pos_neg; first exact: powerRZ_1_even. by rewrite /= Rmult_1_r; apply: Ropp_le_0; apply: Rle_0_1. 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