proposition: Lemma even_power_pos : forall n, Nat.Even n -> forall x : R, x [#] [0] -> [0] [<] x[^]n.
proof: Proof. intros n Hn x Hx. destruct (even_or_odd_plus n) as [k [Hk | Hk]]. - astepr ((x[^]2)[^](k)). apply nexp_resp_pos, pos_square; exact Hx. astepr ((x[^]2)[^](k)); [reflexivity |]. now rewrite nexp_mult, Hk; replace (2 * k) with (k + k) by lia. - exfalso; apply (Nat.Even_Odd_False n); [exact Hn |]. exists k; lia. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)