proposition: Lemma nexp_resp_leEq : forall (x y : R) k, [0] [<=] x -> x [<=] y -> x[^]k [<=] y[^]k.
proof: Proof. intros. rewrite -> leEq_def in *. intro. apply H0. apply power_cancel_less with k; firstorder using leEq_def. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)