proposition: Lemma power_resp_leEq : forall (x y : R) k, [0] [<=] x -> x [<=] y -> x[^]k [<=] y[^]k.
proof: Proof. intros. induction k as [| k Hreck]; intros. astepl ([1]:R). astepr ([1]:R). apply leEq_reflexive. astepl (x[^]k[*]x). astepr (y[^]k[*]y). apply leEq_transitive with (x[^]k[*]y). apply mult_resp_leEq_lft. auto. apply nexp_resp_nonneg; auto. apply mult_resp_leEq_rht. auto. apply leEq_transitive with x; auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)