proposition: Lemma nexp_resp_leEq_odd : forall n, Nat.Odd n -> forall x y : IR, x [<=] y -> x[^]n [<=] y[^]n.
proof: Proof. intros [| n] H x y H'; [destruct H as [m H]; rewrite Nat.add_1_r in H; discriminate H |]. apply Nat.Odd_succ in H. astepl (Part (FId{^}S n) x I). astepr (Part (FId{^}S n) y I). apply Derivative_imp_resp_leEq with realline I (nring (R:=IR) (S n) {**}FId{^}n). Opaque nring. Derivative_Help. FEQ. Transparent nring. auto. split. split. intros. apply leEq_glb; intros. simpl in |- *. apply mult_resp_nonneg. apply less_leEq; eapply leEq_less_trans. 2: apply less_plusOne. apply nring_nonneg. astepr (y0[^]n); apply nexp_even_nonneg. inversion H; auto. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3