proposition: Lemma nexp_resp_nonneg : forall (x : R) (k : nat), [0] [<=] x -> [0] [<=] x[^]k.
proof: Proof. intros. induction k as [| k Hreck]. intros. astepr ([1]:R). apply less_leEq. apply pos_one. astepr (x[^]k[*]x). apply mult_resp_nonneg; auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)