proposition: Lemma nexp_resp_leEq_neg_even : forall n, Nat.Even n -> forall x y : R, y [<=] [0] -> x [<=] y -> y[^]n [<=] x[^]n.
proof: Proof. do 2 intro; pattern n in |- *; apply even_ind; [| | assumption]. intros; simpl in |- *; apply leEq_reflexive. clear H n; intros. astepr (x[^]n[*]x[*]x); astepl (y[^]n[*]y[*]y). astepr (x[^]n[*] (x[*]x)); astepl (y[^]n[*] (y[*]y)). apply mult_resp_leEq_both. eapply leEq_wdr. 2: apply inv_nexp_even; auto. apply nexp_resp_nonneg; astepl ([--] ([0]:R)); apply inv_resp_leEq; auto. astepr (y[^]2); apply sqr_nonneg. auto. astepl (y[^]2); astepr (x[^]2). assert (E : Nat.Even 2) by (now exists 1). eapply leEq_wdr. 2: apply inv_nexp_even; assumption. eapply leEq_wdl. 2: apply inv_nexp_even; assumption. apply nexp_resp_leEq. astepl ([--] ([0]:R)); apply inv_resp_leEq; assumption. apply inv_resp_leEq; assumption. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)