proposition: Lemma nexp_resp_leEq_neg_odd : forall n, Nat.Odd n -> forall x y : R, y [<=] [0] -> x [<=] y -> x[^]n [<=] y[^]n.
proof: Proof. intro; case n; [intros [x H]; rewrite Nat.add_1_r in H; discriminate H |]. clear n; intros n H%Nat.Odd_succ x y Hy Hxy. astepl (x[^]n[*]x); astepr (y[^]n[*]y). rstepl ([--] (x[^]n[*][--]x)); rstepr ([--] (y[^]n[*][--]y)). apply inv_resp_leEq; apply mult_resp_leEq_both. eapply leEq_wdr. 2: { apply inv_nexp_even; inversion H; assumption. } apply nexp_resp_nonneg; astepl ([--] ([0]:R)); apply inv_resp_leEq; auto. astepl ([--] ([0]:R)); apply inv_resp_leEq; auto. apply nexp_resp_leEq_neg_even; auto; inversion H. apply inv_resp_leEq; auto. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)