proposition: Lemma nexp_even_nonneg : forall n, Nat.Even n -> forall x : R, [0] [<=] x[^]n.
proof: Proof. do 2 intro. pattern n in |- *; apply even_ind; intros. simpl in |- *; apply less_leEq; apply pos_one. apply leEq_wdr with (x[^]n0[*]x[^]2). 2: simpl in |- *; rational. apply mult_resp_nonneg. auto. apply sqr_nonneg. auto. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)